let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int A) )
thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int A) ) :: thesis: ( ( for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int 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 (Cl A) = Cl (Int A)
let A be Subset of X; :: thesis: ( A is condensed implies Int (Cl A) = Cl (Int A) )
assume A is condensed ; :: thesis: Int (Cl A) = Cl (Int A)
then A2: Cl A = Cl (Int A) by Th9;
Cl (Int A) is open by A1;
hence Int (Cl A) = Cl (Int A) by A2, TOPS_1:23; :: thesis: verum

end;

assume A3: for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int 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 A4: A is condensed ; :: thesis: ( A is closed & A is open )
then Int (Cl A) = Cl (Int A) by A3;
hence ( A is closed & A is open ) by A4, Th8; :: thesis: verum

end;

hence X is extremally_disconnected by Th32; :: thesis: verum