src/HOL/Topological_Spaces.thy
 changeset 61342 b98cd131e2b5 parent 61306 9dd394c866fc child 61426 d53db136e8fd
equal inserted replaced
61341:e60c7d0bb4b1 61342:b98cd131e2b5
`  1865   obtain sb where sb: "sb \<in> S" "B \<inter> sb \<noteq> {}"`
`  1865   obtain sb where sb: "sb \<in> S" "B \<inter> sb \<noteq> {}"`
`  1866     using Blap by auto`
`  1866     using Blap by auto`
`  1867   obtain x where x: "\<And>s. s \<in> S \<Longrightarrow> x \<in> s"`
`  1867   obtain x where x: "\<And>s. s \<in> S \<Longrightarrow> x \<in> s"`
`  1868     using ne by auto`
`  1868     using ne by auto`
`  1869   then have "x \<in> \<Union>S"`
`  1869   then have "x \<in> \<Union>S"`
`  1870     using `sa \<in> S` by blast`
`  1870     using \<open>sa \<in> S\<close> by blast`
`  1871   then have "x \<in> A \<or> x \<in> B"`
`  1871   then have "x \<in> A \<or> x \<in> B"`
`  1872     using cover by auto`
`  1872     using cover by auto`
`  1873   then show False`
`  1873   then show False`
`  1874     using cs [unfolded connected_def]`
`  1874     using cs [unfolded connected_def]`
`  1875     by (metis A B IntI Sup_upper sa sb disjs x cover empty_iff subset_trans)`
`  1875     by (metis A B IntI Sup_upper sa sb disjs x cover empty_iff subset_trans)`