let Y0, Y1 be TopStruct ; :: thesis: for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds
D1 is T_0
let D0 be Subset of Y0; :: thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds
D1 is T_0
let D1 be Subset of Y1; :: thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 implies D1 is T_0 )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis: ( not D0 = D1 or not D0 is T_0 or D1 is T_0 )
assume A2: D0 = D1 ; :: thesis: ( not D0 is T_0 or D1 is T_0 )
assume A3: D0 is T_0 ; :: thesis: D1 is T_0

now

let x, y be Point of Y1; :: thesis: ( x in D1 & y in D1 & x <> y & ( for V1 being Subset of Y1 holds
( not V1 is open or not x in V1 or y in V1 ) ) implies ex W1 being Subset of Y1 st
( W1 is open & not x in W1 & y in W1 ) )
reconsider x0 = x, y0 = y as Point of Y0 by A1;
assume A4: ( x in D1 & y in D1 ) ; :: thesis: ( not x <> y or 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 ) )
assume A5: x <> y ; :: thesis: ( 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 ) )

hereby :: thesis: verum

per cases ( ex V being Subset of Y0 st
( V is open & x0 in V & not y0 in V ) or ex W being Subset of Y0 st
( W is open & not x0 in W & y0 in W ) ) by A2, A3, A4, A5, Def8;

suppose ex V being Subset of Y0 st
( V is open & x0 in V & not y0 in V ) ; :: thesis: ( 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 ) )

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

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

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: verum

end;

suppose ex W being Subset of Y0 st
( W is open & not x0 in W & y0 in W ) ; :: thesis: ( 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 ) )

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

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

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: verum

end;

end;

end;

end;

hence D1 is T_0 by Def8; :: thesis: verum