[STATEMENT]
lemma chain_glb:
  assumes "transp_on (\<sqsubset>) A"
  shows "chain C \<Longrightarrow> glb (\<sqsubset>) C x \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> chain ({y} \<union> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>chain_on (\<sqsubset>) C A; glb (\<sqsubset>) C x; x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> chain_on (\<sqsubset>) ({y} \<union> C) A
[PROOF STEP]
using assms [unfolded transp_on_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubset> y \<and> y \<sqsubset> z \<longrightarrow> x \<sqsubset> z

goal (1 subgoal):
 1. \<lbrakk>chain_on (\<sqsubset>) C A; glb (\<sqsubset>) C x; x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> chain_on (\<sqsubset>) ({y} \<union> C) A
[PROOF STEP]
unfolding chain_def glb_def lb_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubset> y \<and> y \<sqsubset> z \<longrightarrow> x \<sqsubset> z

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x); Ball C ((\<sqsubseteq>) x) \<and> (\<forall>y. Ball C ((\<sqsubseteq>) y) \<longrightarrow> y \<sqsubseteq> x); x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> {y} \<union> C \<subseteq> A \<and> (\<forall>x\<in>{y} \<union> C. \<forall>y\<in>{y} \<union> C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)
[PROOF STEP]
by (cases "C = {}") blast+