let M, N be non empty TopSpace; ( M is Hausdorff & M,N are_homeomorphic implies N is Hausdorff )
assume A1:
M is Hausdorff
; ( not M,N are_homeomorphic or N is Hausdorff )
assume
M,N are_homeomorphic
; N is Hausdorff
then consider f being Function of N,M such that
A2:
f is being_homeomorphism
by T_0TOPSP:def 1;
A3:
( dom f = [#] N & rng f = [#] M & f is one-to-one & f is continuous & f " is continuous )
by A2, TOPS_2:def 5;
for p, q being Point of N st p <> q holds
ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
proof
let p,
q be
Point of
N;
( p <> q implies ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) )
assume
p <> q
;
ex N1, N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
then consider M1,
M2 being
Subset of
M such that A4:
(
M1 is
open &
M2 is
open &
f . p in M1 &
f . q in M2 &
M1 misses M2 )
by A1, A3, PRE_TOPC:def 10;
reconsider N1 =
f " M1 as
Subset of
N ;
reconsider N2 =
f " M2 as
Subset of
N ;
take
N1
;
ex N2 being Subset of N st
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
take
N2
;
( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )
thus
(
N1 is
open &
N2 is
open )
by A4, A3, TOPS_2:43;
( p in N1 & q in N2 & N1 misses N2 )
thus
(
p in N1 &
q in N2 )
by A4, FUNCT_2:38;
N1 misses N2
thus
N1 misses N2
by A4, FUNCT_1:71;
verum
end;
hence
N is Hausdorff
by PRE_TOPC:def 10; verum