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 is closed )
thus ( X is extremally_disconnected implies for A being Subset of X st A is closed holds
Int A is closed ) :: thesis: ( ( for A being Subset of X st A is closed holds
Int A is closed ) 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 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 Cl (A `) is open by A1;
then (Cl (A `)) ` is closed ;
hence Int A is closed by TOPS_1:def 1; :: thesis: verum
end;
assume A2: for A being Subset of X st A is closed holds
Int A is closed ; :: thesis: X is extremally_disconnected
now :: thesis: for A being Subset of X st A is open holds
Cl A is open
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 Int (A `) is closed by A2;
then (Int (A `)) ` is open ;
hence Cl A is open by Th1; :: thesis: verum
end;
hence X is extremally_disconnected ; :: thesis: verum