[STATEMENT]
lemma connected_disjoint_Union_open_subset:
  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
      and eq [simp]: "\<Union>A = \<Union>B"
    shows "A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
assume "S \<in> A"
[PROOF STATE]
proof (state)
this:
S \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
obtain T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. \<lbrakk>T \<in> B; S \<subseteq> T; S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SA SB \<open>S \<in> A\<close> connected_disjoint_Union_open_pick [OF B, of A] eq order_refl
[PROOF STATE]
proof (prove)
using this:
?S \<in> A \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
?S \<in> B \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
S \<in> A
\<lbrakk>\<And>S. S \<in> A \<Longrightarrow> connected S \<and> S \<noteq> {}; \<And>S. S \<in> B \<Longrightarrow> open S; \<Union> A \<subseteq> \<Union> B; ?S \<in> A; \<And>T. \<lbrakk>T \<in> B; ?S \<subseteq> T; ?S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<Union> A = \<Union> B
?x \<le> ?x

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>T \<in> B; S \<subseteq> T; S \<inter> \<Union> (B - {T}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
obtain S' where "S' \<in> A" "T \<subseteq> S'" "T \<inter> \<Union>(A - {S'}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<in> A; T \<subseteq> S'; T \<inter> \<Union> (A - {S'}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using SA SB \<open>T \<in> B\<close> connected_disjoint_Union_open_pick [OF A, of B] eq order_refl
[PROOF STATE]
proof (prove)
using this:
?S \<in> A \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
?S \<in> B \<Longrightarrow> open ?S \<and> connected ?S \<and> ?S \<noteq> {}
T \<in> B
\<lbrakk>\<And>S. S \<in> B \<Longrightarrow> connected S \<and> S \<noteq> {}; \<And>S. S \<in> A \<Longrightarrow> open S; \<Union> B \<subseteq> \<Union> A; ?S \<in> B; \<And>T. \<lbrakk>T \<in> A; ?S \<subseteq> T; ?S \<inter> \<Union> (A - {T}) = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<Union> A = \<Union> B
?x \<le> ?x

goal (1 subgoal):
 1. (\<And>S'. \<lbrakk>S' \<in> A; T \<subseteq> S'; T \<inter> \<Union> (A - {S'}) = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}
[PROOF STEP]
have "S' = S"
[PROOF STATE]
proof (prove)
using this:
T \<in> B
S \<subseteq> T
S \<inter> \<Union> (B - {T}) = {}
S' \<in> A
T \<subseteq> S'
T \<inter> \<Union> (A - {S'}) = {}

goal (1 subgoal):
 1. S' = S
[PROOF STEP]
by (metis A Int_subset_iff SA \<open>S \<in> A\<close> disjnt_def inf.orderE pairwise_def)
[PROOF STATE]
proof (state)
this:
S' = S

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>T \<subseteq> S'\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<subseteq> S'
S' = S
[PROOF STEP]
have "T \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> S'
S' = S

goal (1 subgoal):
 1. T \<subseteq> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T \<subseteq> S

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>S \<subseteq> T\<close>
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> T
T \<subseteq> S
[PROOF STEP]
have "S = T"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> T
T \<subseteq> S

goal (1 subgoal):
 1. S = T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S = T

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> B
[PROOF STEP]
with \<open>T \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<in> B
S = T
[PROOF STEP]
show "S \<in> B"
[PROOF STATE]
proof (prove)
using this:
T \<in> B
S = T

goal (1 subgoal):
 1. S \<in> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S \<in> B

goal:
No subgoals!
[PROOF STEP]
qed