let X be non empty TopSpace; ( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )
thus
( X is extremally_disconnected implies Domains_Lattice X is M_Lattice )
( Domains_Lattice X is M_Lattice implies X is extremally_disconnected )
assume A1:
Domains_Lattice X is M_Lattice
; X is extremally_disconnected
assume
not X is extremally_disconnected
; 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; verum