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

proof

assume A1: X is extremally_disconnected ; :: thesis: for A, B being Subset of X st A is open & B is open & A misses B holds
Cl A misses Cl B
let A, B be Subset of X; :: thesis: ( A is open & B is open & A misses B implies Cl A misses Cl B )
assume A2: ( A is open & B is open ) ; :: thesis: ( not A misses B or Cl A misses Cl B )
assume A misses B ; :: thesis: Cl A misses Cl B
then ( A misses Cl B & Cl B is open ) by A1, A2, Def4, TSEP_1:40;
hence Cl A misses Cl B by TSEP_1:40; :: thesis: verum

end;

assume A3: for A, B being Subset of X st A is open & B is open & A misses B holds
Cl A misses Cl B ; :: thesis: X is extremally_disconnected

now

let A be Subset of X; :: thesis: ( A is open implies Cl A is open )
assume A4: A is open ; :: thesis: Cl A is open
( 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 A3, A4;
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 is open by XBOOLE_0:def 10; :: thesis: verum

end;

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