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

proof

assume A1: X is extremally_disconnected ; :: thesis: for A being Subset of X st A is closed holds
Int A = Cl (Int A)
let A be Subset of X; :: thesis: ( A is closed implies Int A = Cl (Int A) )
assume A is closed ; :: thesis: Int A = Cl (Int A)
then Cl (A `) = Int (Cl (A `)) by A1, Th30;
then Int A = (Int (((Cl (A `)) `) `)) ` by TOPS_1:def 1;
then Int A = Cl ((Cl (A `)) `) by Th1;
hence Int A = Cl (Int A) ; :: thesis: verum

end;

assume A2: for A being Subset of X st A is closed holds
Int A = Cl (Int A) ; :: thesis: X is extremally_disconnected

now :: thesis: for A being Subset of X st A is closed holds
Int A is closed

let A be Subset of X; :: thesis: ( A is closed implies Int A is closed )
assume A is closed ; :: thesis: Int A is closed
then Int A = Cl (Int A) by A2;
hence Int A is closed ; :: thesis: verum

end;

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