let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )
thus ( X is extremally_disconnected implies Domains_Lattice X is M_Lattice ) :: thesis: ( Domains_Lattice X is M_Lattice implies X is extremally_disconnected ) assume A1: Domains_Lattice X is M_Lattice ; :: thesis: X is extremally_disconnected
assume not X is extremally_disconnected ; :: thesis: contradiction
then consider D being Subset of X such that
A2: D is condensed and
A3: Int (Cl D) <> Cl (Int D) by Th34;
set A = Int (Cl D);
set C = Cl (Int D);
set B = (Cl (Int D)) ` ;
A4: D c= Cl (Int D) by A2, TOPS_1:def 6;
Int (Cl D) c= D by A2, TOPS_1:def 6;
then A5: Int (Cl D) c= Cl (Int D) by A4;
A6: Int (Cl D) is open_condensed by TDLAT_1:23;
then A7: Int (Cl D) = Int (Cl (Int (Cl D))) by TOPS_1:def 8;
(Cl (Int D)) ` misses Cl (Int D) by XBOOLE_1:79;
then A8: ((Cl (Int D)) `) /\ (Cl (Int D)) = {} X ;
A9: Cl (Int D) is closed_condensed by TDLAT_1:22;
then A10: Cl (Int D) = Cl (Int (Cl (Int D))) by TOPS_1:def 7;
Cl (Int D) is condensed by A9, TOPS_1:66;
then A11: Cl (Int D) in { E where E is Subset of X : E is condensed } ;
reconsider c = Cl (Int D) as Element of (Domains_Lattice X) by A11;
Int (Cl D) is condensed by A6, TOPS_1:67;
then Int (Cl D) in { E where E is Subset of X : E is condensed } ;
then reconsider a = Int (Cl D) as Element of (Domains_Lattice X) ;
A15: (Cl (Int D)) ` = Int ((Int D) `) by Th3
.= Int (Cl (D `)) by Th2 ;
((Cl (Int D)) `) ` is closed_condensed by TDLAT_1:22;
then (Cl (Int D)) ` is open_condensed by TOPS_1:61;
then (Cl (Int D)) ` is condensed by TOPS_1:67;
then (Cl (Int D)) ` in { E where E is Subset of X : E is condensed } ;
then reconsider b = (Cl (Int D)) ` as Element of (Domains_Lattice X) ;
A16: (Int (Cl D)) \/ ({} X) = Int (Cl D) ;
Cl ((Int (Cl D)) \/ ((Cl (Int D)) `)) = (Cl (Int (Cl D))) \/ (Cl ((Cl (Int D)) `)) by PRE_TOPC:20
.= Cl (Int ((Cl D) \/ (Cl (D `)))) by A15, TDLAT_1:6
.= Cl (Int (Cl (D \/ (D `)))) by PRE_TOPC:20
.= Cl (Int (Cl ([#] X))) by PRE_TOPC:2
.= Cl (Int ([#] X)) by TOPS_1:2
.= Cl ([#] X) by TOPS_1:15
.= [#] X by TOPS_1:2 ;
then a "\/" b = (Int ([#] X)) \/ ((Int (Cl D)) \/ ((Cl (Int D)) `)) by TDLAT_2:87
.= ([#] X) \/ ((Int (Cl D)) \/ ((Cl (Int D)) `)) by TOPS_1:15
.= [#] X by XBOOLE_1:12 ;
then A17: (a "\/" b) "/\" c = (Cl (Int (([#] X) /\ (Cl (Int D))))) /\ (([#] X) /\ (Cl (Int D))) by TDLAT_2:87
.= (Cl (Int (Cl (Int D)))) /\ (([#] X) /\ (Cl (Int D))) by XBOOLE_1:28
.= (Cl (Int (Cl (Int D)))) /\ (Cl (Int D)) by XBOOLE_1:28
.= Cl (Int D) by A10 ;
A18: a [= c by A5, TDLAT_2:89;
b "/\" c = (Cl (Int (((Cl (Int D)) `) /\ (Cl (Int D))))) /\ (((Cl (Int D)) `) /\ (Cl (Int D))) by TDLAT_2:87
.= {} X by A8 ;
then a "\/" (b "/\" c) = (Int (Cl (Int (Cl D)))) \/ (Int (Cl D)) by A16, TDLAT_2:87
.= Int (Cl D) by A7 ;
hence contradiction by A1, A3, A18, A17, LATTICES:def 12; :: thesis: verum