[STATEMENT]
lemma eq_order_le:
  "\<lbrakk> x=y; order r A; x \<in>A ; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; order r A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; order r A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; (\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> z); x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done