let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )
thus ( X is extremally_disconnected implies for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) :: thesis: ( ( for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) implies X is extremally_disconnected )
proof
assume A1: X is extremally_disconnected ; :: thesis: for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) )
let A be Subset of X; :: thesis: ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) )
thus ( A is open_condensed implies A is closed_condensed ) :: thesis: ( A is closed_condensed implies A is open_condensed )
proof
assume A is open_condensed ; :: thesis: A is closed_condensed
then A is condensed by TOPS_1:67;
hence A is closed_condensed by A1, Th33; :: thesis: verum
end;
thus ( A is closed_condensed implies A is open_condensed ) :: thesis: verum
proof
assume A is closed_condensed ; :: thesis: A is open_condensed
then A is condensed by TOPS_1:66;
hence A is open_condensed by A1, Th33; :: thesis: verum
end;
end;
assume A2: for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ; :: thesis: X is extremally_disconnected
for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int A)
proof
let A be Subset of X; :: thesis: ( A is condensed implies Int (Cl A) = Cl (Int A) )
assume A3: A is condensed ; :: thesis: Int (Cl A) = Cl (Int A)
then A4: A c= Cl (Int A) by TOPS_1:def 6;
Cl (Int A) is closed_condensed by TDLAT_1:22;
then Cl (Int A) is open_condensed by A2;
then Cl (Int A) = Int (Cl (Cl (Int A))) by TOPS_1:def 8;
then A5: Cl (Int A) c= Int (Cl A) by TDLAT_2:1;
Int (Cl A) c= A by A3, TOPS_1:def 6;
then Int (Cl A) c= Cl (Int A) by A4;
hence Int (Cl A) = Cl (Int A) by A5; :: thesis: verum
end;
hence X is extremally_disconnected by Th34; :: thesis: verum