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:107;
hence A is closed_condensed by A1, Th35; :: 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:106;
hence A is open_condensed by A1, Th35; :: 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 A is condensed ; :: thesis: Int (Cl A) = Cl (Int A)
then ( Int (Cl A) c= A & A c= Cl (Int A) ) by TOPS_1:def 6;
then A3: Int (Cl A) c= Cl (Int A) by XBOOLE_1:1;
( Int (Cl A) is open_condensed & Cl (Int A) is closed_condensed ) by TDLAT_1:22, TDLAT_1:23;
then ( Int (Cl A) is closed_condensed & Cl (Int A) is open_condensed ) by A2;
then ( Int (Cl A) = Cl (Int (Int (Cl A))) & Cl (Int A) = Int (Cl (Cl (Int A))) ) by TOPS_1:def 7, TOPS_1:def 8;
then Cl (Int A) c= Int (Cl A) by TDLAT_2:1;
hence Int (Cl A) = Cl (Int A) by A3, XBOOLE_0:def 10; :: thesis: verum

end;

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