reconsider A = the carrier of Y0 as Subset of Y by Lm3;
thus ( not Y0 is T_0 or Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) :: thesis: ( ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) implies Y0 is T_0 )
proof
assume A1: Y0 is T_0 ; :: thesis: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) )

hereby :: thesis: verum
assume A2: not Y0 is empty ; :: thesis: for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is open or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is open & not x in F & y in F )

let x, y be Point of Y; :: thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is open or not x in E or y in E ) ) implies ex F being Subset of Y st
( F is open & not x in F & y in F ) )

assume ( x is Point of Y0 & y is Point of Y0 ) ; :: thesis: ( not x <> y or ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )

then reconsider x0 = x, y0 = y as Point of Y0 ;
assume A3: x <> y ; :: thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )

now :: thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
per cases ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
by A1, A2, A3;
suppose ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) ; :: thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )

then consider E0 being Subset of Y0 such that
A4: E0 is open and
A5: x0 in E0 and
A6: not y0 in E0 ;
now :: thesis: ex E being Subset of Y st
( E is open & x in E & not y in E )
consider E being Subset of Y such that
A7: E is open and
A8: E0 = E /\ A by ;
take E = E; :: thesis: ( E is open & x in E & not y in E )
thus E is open by A7; :: thesis: ( x in E & not y in E )
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5, A8; :: thesis: not y in E
thus not y in E by ; :: thesis: verum
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; :: thesis: verum
end;
suppose ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ; :: thesis: ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )

then consider F0 being Subset of Y0 such that
A9: F0 is open and
A10: not x0 in F0 and
A11: y0 in F0 ;
now :: thesis: ex F being Subset of Y st
( F is open & not x in F & y in F )
consider F being Subset of Y such that
A12: F is open and
A13: F0 = F /\ A by ;
take F = F; :: thesis: ( F is open & not x in F & y in F )
thus F is open by A12; :: thesis: ( not x in F & y in F )
thus not x in F by ; :: thesis: y in F
F /\ A c= F by XBOOLE_1:17;
hence y in F by ; :: thesis: verum
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; :: thesis: verum
end;
end;
end;
hence ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) ) ; :: thesis: verum
end;
end;
assume A14: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis: Y0 is T_0
now :: thesis: ( not Y0 is empty implies for x0, y0 being Point of Y0 holds
( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) )
A15: the carrier of Y0 c= the carrier of Y by Def1;
assume A16: not Y0 is empty ; :: thesis: for x0, y0 being Point of Y0 holds
( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )

let x0, y0 be Point of Y0; :: thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )

the carrier of Y0 <> {} by A16;
then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;
then reconsider x = x0, y = y0 as Point of Y by A15;
assume A17: x0 <> y0 ; :: thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )

now :: thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )
per cases ( ex E being Subset of Y st
( E is open & x in E & not y in E ) or ex F being Subset of Y st
( F is open & not x in F & y in F ) )
by ;
suppose ex E being Subset of Y st
( E is open & x in E & not y in E ) ; :: thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )

then consider E being Subset of Y such that
A18: E is open and
A19: x in E and
A20: not y in E ;
now :: thesis: ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 )
consider E0 being Subset of Y0 such that
A21: E0 is open and
A22: E0 = E /\ A by ;
take E0 = E0; :: thesis: ( E0 is open & x0 in E0 & not y0 in E0 )
thus E0 is open by A21; :: thesis: ( x0 in E0 & not y0 in E0 )
thus x0 in E0 by ; :: thesis: not y0 in E0
now :: thesis: not y0 in E0end;
hence not y0 in E0 ; :: thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum
end;
suppose ex F being Subset of Y st
( F is open & not x in F & y in F ) ; :: thesis: ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) )

then consider F being Subset of Y such that
A24: F is open and
A25: not x in F and
A26: y in F ;
now :: thesis: ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 )
consider F0 being Subset of Y0 such that
A27: F0 is open and
A28: F0 = F /\ A by ;
take F0 = F0; :: thesis: ( F0 is open & not x0 in F0 & y0 in F0 )
thus F0 is open by A27; :: thesis: ( not x0 in F0 & y0 in F0 )
now :: thesis: not x0 in F0end;
hence not x0 in F0 ; :: thesis: y0 in F0
thus y0 in F0 by ; :: thesis: verum
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum
end;
end;
end;
hence ( ex E0 being Subset of Y0 st
( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st
( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum
end;
hence Y0 is T_0 ; :: thesis: verum