let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int A = Cl A )
thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds
Int A = Cl A ) :: thesis: ( ( for A being Subset of X st A is condensed holds
Int A = Cl A ) implies X is extremally_disconnected )
proof
assume A1: X is extremally_disconnected ; :: thesis: for A being Subset of X st A is condensed holds
Int A = Cl A
let A be Subset of X; :: thesis: ( A is condensed implies Int A = Cl A )
assume A2: A is condensed ; :: thesis: Int A = Cl A
then A is closed by A1, Th32;
then A3: A = Cl A by PRE_TOPC:22;
A is open by A1, A2, Th32;
hence Int A = Cl A by A3, TOPS_1:23; :: thesis: verum
end;
assume A4: for A being Subset of X st A is condensed holds
Int A = Cl A ; :: thesis: X is extremally_disconnected
now :: thesis: for A being Subset of X st A is condensed holds
( A is closed & A is open )
let A be Subset of X; :: thesis: ( A is condensed implies ( A is closed & A is open ) )
assume A is condensed ; :: thesis: ( A is closed & A is open )
then Int A = Cl A by A4;
hence ( A is closed & A is open ) by Th5; :: thesis: verum
end;
hence X is extremally_disconnected by Th32; :: thesis: verum