let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
( A is closed & A is open ) )
thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds
( A is closed & A is open ) ) :: thesis: ( ( for A being Subset of X st A is condensed holds
( A is closed & A is open ) ) implies X is extremally_disconnected )

proof

assume A1: X is extremally_disconnected ; :: 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 A2: A is condensed ; :: thesis: ( A is closed & A is open )
then A3: Cl A = Cl (Int A) by Th11;
Cl (Int A) is open by A1, Def4;
then Int (Cl A) = Cl (Int A) by A3, TOPS_1:55;
hence ( A is closed & A is open ) by A2, Th10; :: thesis: verum

end;

assume A4: for A being Subset of X st A is condensed holds
( A is closed & A is open ) ; :: thesis: X is extremally_disconnected

now

let A be Subset of X; :: thesis: ( A is open implies Cl A is open )
assume A is open ; :: thesis: Cl A is open
then ( Int A = A & Cl (Int A) is closed_condensed ) by TDLAT_1:22, TOPS_1:55;
then Cl A is condensed by TOPS_1:106;
hence Cl A is open by A4; :: thesis: verum

end;

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