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 )
A1: the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by BORSUK_1:def 5;
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;

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 A2: 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 A2, Th45; :: thesis: verum

end;

assume A3: for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed ; :: thesis: T is Hausdorff
A4: [#] [:T,T:] = [:([#] T),([#] T):] by BORSUK_1:def 5;
reconsider A = id the carrier of T as Subset of [:T,T:] by BORSUK_1:def 5;
let p, q be Point of T; :: according to PRE_TOPC:def 16 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A5: not p = q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
A is closed by A3;
then [:([#] T),([#] T):] \ A is open by A4, PRE_TOPC:def 6;
then consider SF being Subset-Family of [:T,T:] such that
A6: [:([#] T),([#] T):] \ A = union SF and
A7: 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:45;
not [p,q] in id ([#] T) by A5, RELAT_1:def 10;
then [p,q] in [:([#] T),([#] T):] \ A by A1, XBOOLE_0:def 5;
then consider XY being set such that
A8: ( [p,q] in XY & XY in SF ) by A6, TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A9: ( XY = [:X1,Y1:] & X1 is open & Y1 is open ) by A7, A8;
take X1 ; :: thesis: ex b₁ being Element of bool the carrier of T st
( X1 is open & b₁ is open & p in X1 & q in b₁ & X1 misses b₁ )
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 A9; :: thesis: ( p in X1 & q in Y1 & X1 misses Y1 )
thus ( p in X1 & q in Y1 ) by A8, A9, ZFMISC_1:106; :: thesis: X1 misses Y1
assume X1 /\ Y1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider w being set such that
A10: w in X1 /\ Y1 by XBOOLE_0:def 1;
( w in X1 & w in Y1 ) by A10, XBOOLE_0:def 4;
then [w,w] in XY by A9, ZFMISC_1:106;
then [w,w] in union SF by A8, TARSKI:def 4;
then not [w,w] in A by A6, XBOOLE_0:def 5;
hence contradiction by A10, RELAT_1:def 10; :: thesis: verum