let M, N be non empty TopSpace; :: thesis: ( M is T_2 & M,N are_homeomorphic implies N is T_2 )
assume A1: M is T_2 ; :: thesis: ( not M,N are_homeomorphic or N is T_2 )
assume M,N are_homeomorphic ; :: thesis: N is T_2
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; :: 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 f . p <> f . q by A3, FUNCT_1:def 4;
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, 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;

hence N is T_2 by PRE_TOPC:def 10; :: thesis: verum