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 E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) :: thesis:

proof

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 A4: x <> y ; :: thesis:

now

per cases by A1, A2, A4, Def4;

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

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

now

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

end;

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

end;

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

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

now

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

end;

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

end;

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

end;

assume A15: ( 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 E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) ; :: thesis:

now

assume A16: not Y0 is empty ; :: thesis:
let x0, y0 be Point of Y0; :: thesis:
the carrier of Y0 <> {} by A16;
then A18: ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;
the carrier of Y0 c= the carrier of Y by Def1;
then reconsider x = x0, y = y0 as Point of Y by A18;
assume A19: x0 <> y0 ; :: thesis:

now

per cases by A15, A16, A19;

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

then consider E being Subset of Y such that
A20: E is closed and
A21: x in E and
A22: not y in E ;

now

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

now

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

end;

hence not y0 in E0 ; :: thesis:

end;

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

end;

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

then consider F being Subset of Y such that
A26: F is closed and
A27: not x in F and
A28: y in F ;

now

consider F0 being Subset of Y0 such that
A29: F0 is closed and
A30: F0 = F /\ A by A26, Th4;
take F0 = F0; :: thesis:
thus F0 is closed by A29; :: thesis:

now

assume A31: x0 in F0 ; :: thesis:
F /\ A c= F by XBOOLE_1:17;
hence contradiction by A27, A30, A31; :: thesis:

end;

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

end;

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

end;

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

end;

hence Y0 is T_0 by Def4; :: thesis: