let Y0, Y1 be TopStruct ; :: thesis:
let D0 be Subset of Y0; :: thesis:
let D1 be Subset of Y1; :: thesis:
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis:
assume A2: D0 = D1 ; :: thesis:
assume A3: D0 is T_0 ; :: thesis:

now :: thesis:

let x, y be Point of Y1; :: thesis:
reconsider x0 = x, y0 = y as Point of Y0 by A1;
assume A4: ( x in D1 & y in D1 ) ; :: thesis:
assume A5: x <> y ; :: thesis:

hereby :: thesis:

per cases by A2, A3, A4, A5;

suppose ex V being Subset of Y0 st
( V is open & x0 in V & not y0 in V ) ; :: thesis:

then consider V being Subset of Y0 such that
A6: V is open and
A7: ( x0 in V & not y0 in V ) ;
reconsider V1 = V as Subset of Y1 by A1;

now :: thesis:

take V1 = V1; :: thesis:
V1 in the topology of Y1 by A1, A6, PRE_TOPC:def 2;
hence V1 is open by PRE_TOPC:def 2; :: thesis:
thus ( x in V1 & not y in V1 ) by A7; :: thesis:

end;

hence ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) ) ; :: thesis:

end;

suppose ex W being Subset of Y0 st
( W is open & not x0 in W & y0 in W ) ; :: thesis:

then consider W being Subset of Y0 such that
A8: W is open and
A9: ( not x0 in W & y0 in W ) ;
reconsider W1 = W as Subset of Y1 by A1;

now :: thesis:

take W1 = W1; :: thesis:
W1 in the topology of Y1 by A1, A8, PRE_TOPC:def 2;
hence W1 is open by PRE_TOPC:def 2; :: thesis:
thus ( not x in W1 & y in W1 ) by A9; :: thesis:

end;

hence ( ex V1 being Subset of Y1 st
( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) ) ; :: thesis:

end;

end;

end;

end;

hence D1 is T_0 ; :: thesis: