let M, N be non empty TopSpace; :: thesis: ( M is Hausdorff & M,N are_homeomorphic implies N is Hausdorff )

assume A1: M is Hausdorff ; :: thesis: ( not M,N are_homeomorphic or N is Hausdorff )

assume M,N are_homeomorphic ; :: thesis: 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 )

assume A1: M is Hausdorff ; :: thesis: ( not M,N are_homeomorphic or N is Hausdorff )

assume M,N are_homeomorphic ; :: thesis: 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

hence
N is Hausdorff
by PRE_TOPC:def 10; :: thesis: verum
let p, q be Point of N; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex N2 being Subset of N st

( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )

take N2 ; :: thesis: ( 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; :: thesis: ( p in N1 & q in N2 & N1 misses N2 )

thus ( p in N1 & q in N2 ) by A4, FUNCT_2:38; :: thesis: N1 misses N2

thus N1 misses N2 by A4, FUNCT_1:71; :: thesis: verum

end;( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 ) )

assume p <> q ; :: thesis: 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 ; :: thesis: ex N2 being Subset of N st

( N1 is open & N2 is open & p in N1 & q in N2 & N1 misses N2 )

take N2 ; :: thesis: ( 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; :: thesis: ( p in N1 & q in N2 & N1 misses N2 )

thus ( p in N1 & q in N2 ) by A4, FUNCT_2:38; :: thesis: N1 misses N2

thus N1 misses N2 by A4, FUNCT_1:71; :: thesis: verum