let T be non empty TopSpace; :: thesis: ( T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed )
reconsider f = pr1 ( the carrier of T, the carrier of T), g = pr2 ( the carrier of T, the carrier of T) as continuous Function of [:T,T:],T by Th39, Th40;
reconsider A = id the carrier of T as Subset of [:T,T:] by BORSUK_1:def 2;
hereby :: thesis: ( ( for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed ) implies T is Hausdorff )
assume A1: T is Hausdorff ; :: thesis: for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed
let A be Subset of [:T,T:]; :: thesis: ( A = id the carrier of T implies A is closed )
assume A = id the carrier of T ; :: thesis: A is closed
then A = { p where p is Point of [:T,T:] : f . p = g . p } by Th37;
hence A is closed by A1, Th45; :: thesis: verum
end;
assume for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed ; :: thesis: T is Hausdorff
then ( [#] [:T,T:] = [:([#] T),([#] T):] & A is closed ) by BORSUK_1:def 2;
then [:([#] T),([#] T):] \ A is open ;
then consider SF being Subset-Family of [:T,T:] such that
A2: [:([#] T),([#] T):] \ A = union SF and
A3: for e being set st e in SF holds
ex X1, Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
let p, q be Point of T; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume not p = q ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then ( the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] & not [p,q] in id ([#] T) ) by BORSUK_1:def 2, RELAT_1:def 10;
then [p,q] in [:([#] T),([#] T):] \ A by XBOOLE_0:def 5;
then consider XY being set such that
A4: [p,q] in XY and
A5: XY in SF by A2, TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A6: XY = [:X1,Y1:] and
A7: ( X1 is open & Y1 is open ) by A3, A5;
take X1 ; :: thesis: ex b1 being Element of bool the carrier of T st
( X1 is open & b1 is open & p in X1 & q in b1 & X1 misses b1 )
take Y1 ; :: thesis: ( X1 is open & Y1 is open & p in X1 & q in Y1 & X1 misses Y1 )
thus ( X1 is open & Y1 is open ) by A7; :: thesis: ( p in X1 & q in Y1 & X1 misses Y1 )
thus ( p in X1 & q in Y1 ) by A4, A6, ZFMISC_1:87; :: thesis: X1 misses Y1
assume X1 /\ Y1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider w being object such that
A8: w in X1 /\ Y1 by XBOOLE_0:def 1;
( w in X1 & w in Y1 ) by A8, XBOOLE_0:def 4;
then [w,w] in XY by A6, ZFMISC_1:87;
then [w,w] in union SF by A5, TARSKI:def 4;
then not [w,w] in A by A2, XBOOLE_0:def 5;
hence contradiction by A8, RELAT_1:def 10; :: thesis: verum