reconsider A = the carrier of Y0 as Subset of by Lm3;
thus ( not Y0 is T_0 or Y0 is empty or for x, y being Point of st x is Point of & y is Point of & x <> y & ( for E being Subset of holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of st
( F is closed & not x in F & y in F ) ) :: thesis:

assume A1: Y0 is T_0 ; :: thesis:

hereby :: thesis:

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

now

per cases by A1, A2, A3, Def4;

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

then consider E0 being Subset of such that
A4: E0 is closed and
A5: x0 in E0 and
A6: not y0 in E0 ;

now

consider E being Subset of such that
A7: E is closed and
A8: E0 = E /\ A by A4, Def2;
take E = E; :: thesis:
thus E is closed 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 st
( E is closed & x in E & not y in E ) or ex F being Subset of st
( F is closed & not x in F & y in F ) ) ; :: thesis:

end;

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

then consider F0 being Subset of such that
A9: F0 is closed and
A10: not x0 in F0 and
A11: y0 in F0 ;

now

consider F being Subset of such that
A12: F is closed and
A13: F0 = F /\ A by A9, Def2;
take F = F; :: thesis:
thus F is closed 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 st
( E is closed & x in E & not y in E ) or ex F being Subset of st
( F is closed & not x in F & y in F ) ) ; :: thesis:

end;

hence ( ex E being Subset of st
( E is closed & x in E & not y in E ) or ex F being Subset of st
( F is closed & not x in F & y in F ) ) ; :: thesis:

end;

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

now

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 ; :: 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 by A15;
assume A17: x0 <> y0 ; :: thesis:

now

per cases by A14, A16, A17;

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

then consider E being Subset of such that
A18: E is closed and
A19: x in E and
A20: not y in E ;

now

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

now

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 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; :: thesis:

end;

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

then consider F being Subset of such that
A24: F is closed and
A25: not x in F and
A26: y in F ;

now

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

now

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 st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; :: thesis:

end;

hence ( ex E0 being Subset of st
( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of st
( F0 is closed & not x0 in F0 & y0 in F0 ) ) ; :: thesis:

end;

hence Y0 is T_0 by Def4; :: thesis: