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 that
A3: D0 is open and
A4: B0 is open ; :: thesis: ( not D0 misses B0 or Cl D0 misses Cl B0 )
consider D being Subset of X such that
A5: D is open and
A6: D /\ ([#] X0) = D0 by A3, TOPS_2:24;
consider B being Subset of X such that
A7: B is open and
A8: B /\ ([#] X0) = B0 by A4, TOPS_2:24;
assume A9: D0 /\ B0 = {} ; :: according to XBOOLE_0:def 7 :: thesis: Cl D0 misses Cl B0
D misses B
proof
assume D /\ B <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then D /\ B meets A by A2, A5, A7, TOPS_1:45;
then (D /\ B) /\ A <> {} ;
then D /\ (B /\ (A /\ A)) <> {} by XBOOLE_1:16;
then D /\ (A /\ (B /\ A)) <> {} by XBOOLE_1:16;
hence contradiction by A1, A6, A8, A9, XBOOLE_1:16; :: thesis: verum
end;
then Cl D misses Cl B by A5, A7, Th28;
then (Cl D) /\ (Cl B) = {} ;
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 A10: ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) = {} by XBOOLE_1:16;
A11: Cl B0 c= (Cl B) /\ ([#] X0)
proof
B0 c= B by A8, XBOOLE_1:17;
then reconsider B1 = B0 as Subset of X by XBOOLE_1:1;
Cl B1 c= Cl B by A8, PRE_TOPC:19, XBOOLE_1:17;
then (Cl B1) /\ ([#] X0) c= (Cl B) /\ ([#] X0) by XBOOLE_1:26;
hence Cl B0 c= (Cl B) /\ ([#] X0) by PRE_TOPC:17; :: thesis: verum
end;
Cl D0 c= (Cl D) /\ ([#] X0)
proof
D0 c= D by A6, XBOOLE_1:17;
then reconsider D1 = D0 as Subset of X by XBOOLE_1:1;
Cl D1 c= Cl D by A6, PRE_TOPC:19, XBOOLE_1:17;
then (Cl D1) /\ ([#] X0) c= (Cl D) /\ ([#] X0) by XBOOLE_1:26;
hence Cl D0 c= (Cl D) /\ ([#] X0) by PRE_TOPC:17; :: thesis: verum
end;
then (Cl D0) /\ (Cl B0) c= ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) by A11, XBOOLE_1:27;
then (Cl D0) /\ (Cl B0) = {} by A10;
hence Cl D0 misses Cl B0 ; :: thesis: verum
end;
hence X0 is extremally_disconnected by Th28; :: thesis: verum