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:

assume A1: Y0 is T_0 ; :: thesis:

hereby :: thesis:

assume A2: not Y0 is empty ; :: thesis:
let x, y be Point of Y; :: thesis:
assume ( x is Point of Y0 & y is Point of Y0 ) ; :: thesis:
then reconsider x0 = x, y0 = y as Point of Y0 ;
assume A3: x <> y ; :: thesis:

now :: thesis:

per cases by A1, A2, A3;

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

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:

consider E being Subset of Y such that
A7: E is open and
A8: E0 = E /\ A by A4, Def1;
take E = E; :: thesis:
thus E is open by A7; :: thesis:
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5, A8; :: thesis:
thus not y in E by A2, A6, A8, XBOOLE_0:def 4; :: thesis:

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:

end;

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

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:

consider F being Subset of Y such that
A12: F is open and
A13: F0 = F /\ A by A9, Def1;
take F = F; :: thesis:
thus F is open by A12; :: thesis:
thus not x in F by A2, A10, A13, XBOOLE_0:def 4; :: thesis:
F /\ A c= F by XBOOLE_1:17;
hence y in F by A11, A13; :: thesis:

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:

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:

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:

now :: thesis:

A15: the carrier of Y0 c= the carrier of Y by Def1;
assume A16: not Y0 is empty ; :: thesis:
let x0, y0 be Point of Y0; :: thesis:
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:

now :: thesis:

per cases by A14, A16, A17;

suppose ex E being Subset of Y st
( E is open & x in E & not y in E ) ; :: thesis:

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:

consider E0 being Subset of Y0 such that
A21: E0 is open and
A22: E0 = E /\ A by A18, Th1;
take E0 = E0; :: thesis:
thus E0 is open by A21; :: thesis:
thus x0 in E0 by A16, A19, A22, XBOOLE_0:def 4; :: thesis:

now :: thesis:

A23: E /\ A c= E by XBOOLE_1:17;
assume y0 in E0 ; :: thesis:
hence contradiction by A20, A22, A23; :: thesis:

end;

hence not y0 in E0 ; :: thesis:

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:

end;

suppose ex F being Subset of Y st
( F is open & not x in F & y in F ) ; :: thesis:

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:

consider F0 being Subset of Y0 such that
A27: F0 is open and
A28: F0 = F /\ A by A24, Th1;
take F0 = F0; :: thesis:
thus F0 is open by A27; :: thesis:

now :: thesis:

A29: F /\ A c= F by XBOOLE_1:17;
assume x0 in F0 ; :: thesis:
hence contradiction by A25, A28, A29; :: thesis:

end;

hence not x0 in F0 ; :: thesis:
thus y0 in F0 by A16, A26, A28, XBOOLE_0:def 4; :: thesis:

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:

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:

end;

hence Y0 is T_0 ; :: thesis: