[STATEMENT]
lemma torder_on_restrictPI':
  "\<lbrakk> torder_on A r; B = A \<inter> C \<rbrakk> \<Longrightarrow> torder_on B (r |` C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>torder_on A r; B = A \<inter> C\<rbrakk> \<Longrightarrow> torder_on B (r |` C)
[PROOF STEP]
by(simp add: torder_on_restrictPI)