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

proof

assume A1: X is extremally_disconnected ; :: thesis: for A being Subset of X st A is open holds
Cl A = Int (Cl A)
let A be Subset of X; :: thesis: ( A is open implies Cl A = Int (Cl A) )
assume A2: A is open ; :: thesis: Cl A = Int (Cl A)
( A c= Cl A & Cl A is closed ) by PRE_TOPC:48;
then ( A misses (Cl A) ` & (Cl A) ` is open ) by SUBSET_1:44;
then Cl A misses Cl ((Cl A) ` ) by A1, A2, Th30;
then Cl A c= (Cl ((Cl A) ` )) ` by SUBSET_1:43;
then ( Cl A c= Int (Cl A) & Int (Cl A) c= Cl A ) by TOPS_1:44, TOPS_1:def 1;
hence Cl A = Int (Cl A) by XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

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