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 that
A2: A is open and
A3: 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 A4: A misses Cl B by A2, TSEP_1:36;
Cl B is open by A1, A3;
hence Cl A misses Cl B by A4, TSEP_1:36; :: thesis: verum
end;
assume A5: 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 :: 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 )
A c= Cl A by PRE_TOPC:18;
then A6: A misses (Cl A) ` by SUBSET_1:24;
assume A is open ; :: thesis: Cl A is open
then Cl A misses Cl ((Cl A) `) by A5, A6;
then Cl A c= (Cl ((Cl A) `)) ` by SUBSET_1:23;
then A7: Cl A c= Int (Cl A) by TOPS_1:def 1;
Int (Cl A) c= Cl A by TOPS_1:16;
hence Cl A is open by A7, XBOOLE_0:def 10; :: thesis: verum
end;
hence X is extremally_disconnected ; :: thesis: verum