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_condensed & A is open_condensed ) )
thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds
( A is closed_condensed & A is open_condensed ) ) :: thesis: ( ( for A being Subset of X st A is condensed holds
( A is closed_condensed & A is open_condensed ) ) 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_condensed & A is open_condensed )
let A be Subset of X; :: thesis: ( A is condensed implies ( A is closed_condensed & A is open_condensed ) )
assume A2: A is condensed ; :: thesis: ( A is closed_condensed & A is open_condensed )
then A3: A is open by A1, Th34;
A is closed by A1, A2, Th34;
hence ( A is closed_condensed & A is open_condensed ) by A2, A3, TOPS_1:66, TOPS_1:67; :: thesis: verum

end;

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

now

let A be Subset of X; :: thesis: ( A is condensed implies ( A is closed & A is open ) )
assume A5: A is condensed ; :: thesis: ( A is closed & A is open )
then A6: A is open_condensed by A4;
A is closed_condensed by A4, A5;
hence ( A is closed & A is open ) by A6, TOPS_1:66, TOPS_1:67; :: thesis: verum

end;

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