let T be non empty TopSpace; ( 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;
assume
for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed
; 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; PRE_TOPC:def 10 ( 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
; 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
; 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
; ( X1 is open & Y1 is open & p in X1 & q in Y1 & X1 misses Y1 )
thus
( X1 is open & Y1 is open )
by A7; ( p in X1 & q in Y1 & X1 misses Y1 )
thus
( p in X1 & q in Y1 )
by A4, A6, ZFMISC_1:87; X1 misses Y1
assume
X1 /\ Y1 <> {}
; XBOOLE_0:def 7 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; verum