[STATEMENT]
lemma PO_refines_implies_Range_invariant:
  "PO_refines R Ta Tc \<Longrightarrow> reach Tc \<subseteq> Range R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PO_refines R Ta Tc \<Longrightarrow> reach Tc \<subseteq> Range R
[PROOF STEP]
by (rule INV_rule)
   (auto intro!: PO_refines_implies_Range_init 
                 PO_refines_implies_Range_trans)