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) )
A c= Cl A by PRE_TOPC:18;
then A2: A misses (Cl A) ` by SUBSET_1:24;
assume A is open ; :: thesis: Cl A = Int (Cl A)
then Cl A misses Cl ((Cl A) `) by A1, A2, Th28;
then Cl A c= (Cl ((Cl A) `)) ` by SUBSET_1:23;
then A3: Cl A c= Int (Cl A) by TOPS_1:def 1;
Int (Cl A) c= Cl A by TOPS_1:16;
hence Cl A = Int (Cl A) by A3; :: thesis: verum
end;
assume A4: for A being Subset of X st A is open holds
Cl A = Int (Cl A) ; :: 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 Cl A = Int (Cl A) by A4;
hence Cl A is open ; :: thesis: verum
end;
hence X is extremally_disconnected ; :: thesis: verum