let X be non empty extremally_disconnected TopSpace; :: thesis: for X0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of X0 & A is dense holds
X0 is extremally_disconnected
let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 & A is dense holds
X0 is extremally_disconnected
let A be Subset of X; :: thesis: ( A = the carrier of X0 & A is dense implies X0 is extremally_disconnected )
assume A1: A = the carrier of X0 ; :: thesis: ( not A is dense or X0 is extremally_disconnected )
assume A2: A is dense ; :: thesis: X0 is extremally_disconnected
for D0, B0 being Subset of X0 st D0 is open & B0 is open & D0 misses B0 holds
Cl D0 misses Cl B0

proof

let D0, B0 be Subset of X0; :: thesis: ( D0 is open & B0 is open & D0 misses B0 implies Cl D0 misses Cl B0 )
assume A3: ( D0 is open & B0 is open ) ; :: thesis: ( not D0 misses B0 or Cl D0 misses Cl B0 )
then consider D being Subset of X such that
A4: D is open and
A5: D /\ ([#] X0) = D0 by TOPS_2:32;
consider B being Subset of X such that
A6: B is open and
A7: B /\ ([#] X0) = B0 by A3, TOPS_2:32;
assume A8: D0 /\ B0 = {} ; :: according to XBOOLE_0:def 7 :: thesis: Cl D0 misses Cl B0
A9: Cl D0 c= (Cl D) /\ ([#] X0)

proof

D0 c= D by A5, XBOOLE_1:17;
then reconsider D1 = D0 as Subset of X by XBOOLE_1:1;
Cl D1 c= Cl D by A5, PRE_TOPC:49, XBOOLE_1:17;
then ( (Cl D1) /\ ([#] X0) c= (Cl D) /\ ([#] X0) & Cl D0 = (Cl D1) /\ ([#] X0) ) by PRE_TOPC:47, XBOOLE_1:26;
hence Cl D0 c= (Cl D) /\ ([#] X0) ; :: thesis: verum

end;

A10: Cl B0 c= (Cl B) /\ ([#] X0)

proof

B0 c= B by A7, XBOOLE_1:17;
then reconsider B1 = B0 as Subset of X by XBOOLE_1:1;
Cl B1 c= Cl B by A7, PRE_TOPC:49, XBOOLE_1:17;
then ( (Cl B1) /\ ([#] X0) c= (Cl B) /\ ([#] X0) & Cl B0 = (Cl B1) /\ ([#] X0) ) by PRE_TOPC:47, XBOOLE_1:26;
hence Cl B0 c= (Cl B) /\ ([#] X0) ; :: thesis: verum

end;

D misses B

proof

assume A11: D /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
D /\ B is open by A4, A6, TOPS_1:38;
then D /\ B meets A by A2, A11, TOPS_1:80;
then (D /\ B) /\ A <> {} by XBOOLE_0:def 7;
then D /\ (B /\ (A /\ A)) <> {} by XBOOLE_1:16;
then D /\ (A /\ (B /\ A)) <> {} by XBOOLE_1:16;
hence contradiction by A1, A5, A7, A8, XBOOLE_1:16; :: thesis: verum

end;

then Cl D misses Cl B by A4, A6, Th30;
then (Cl D) /\ (Cl B) = {} by XBOOLE_0:def 7;
then ((Cl D) /\ (Cl B)) /\ ([#] X0) = {} ;
then (Cl D) /\ ((Cl B) /\ (([#] X0) /\ ([#] X0))) = {} by XBOOLE_1:16;
then (Cl D) /\ (([#] X0) /\ ((Cl B) /\ ([#] X0))) = {} by XBOOLE_1:16;
then ( ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) = {} & (Cl D0) /\ (Cl B0) c= ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) ) by A9, A10, XBOOLE_1:16, XBOOLE_1:27;
then (Cl D0) /\ (Cl B0) = {} ;
hence Cl D0 misses Cl B0 by XBOOLE_0:def 7; :: thesis: verum

end;

hence X0 is extremally_disconnected by Th30; :: thesis: verum