thus ( not Y is T_0 or Y is empty or for x, y being Point of holds
( not x <> y or 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: ( ( Y is empty or for x, y being Point of holds
( not x <> y or 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 ) ) ) implies Y is T_0 )

proof

assume A1: ( Y is empty or for x, y being Point of holds
( not x <> y or ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) ) ) ; :: according to TSP_1:def 3 :: thesis: ( Y is empty or for x, y being Point of holds
( not x <> y or 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 ) ) )
assume A2: not Y is empty ; :: thesis: for x, y being Point of holds
( not x <> y or 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 ) )
let x, y be Point of ; :: thesis: ( not x <> y or 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 ) )
assume A3: x <> y ; :: thesis: ( 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 ) )

hereby :: thesis: verum

per cases ( ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) ) by A1, A2, A3;

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

then consider V being Subset of such that
A4: V is open and
A5: x in V and
A6: not y in V ;

now

take F = V ` ; :: thesis: ( F is closed & not x in F & y in F )
V = ([#] Y) \ F by PRE_TOPC:22;
hence F is closed by A4, PRE_TOPC:def 6; :: thesis: ( not x in F & y in F )
thus not x in F by A5, XBOOLE_0:def 5; :: thesis: y in F
thus y in F by A2, A6, SUBSET_1:50; :: thesis: verum

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

end;

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

then consider W being Subset of such that
A7: W is open and
A8: not x in W and
A9: y in W ;

now

take E = W ` ; :: thesis: ( E is closed & x in E & not y in E )
W = ([#] Y) \ E by PRE_TOPC:22;
hence E is closed by A7, PRE_TOPC:def 6; :: thesis: ( x in E & not y in E )
thus x in E by A2, A8, SUBSET_1:50; :: thesis: not y in E
thus not y in E by A9, XBOOLE_0:def 5; :: thesis: verum

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

end;

end;

end;

end;

assume A10: ( Y is empty or for x, y being Point of holds
( not x <> y or 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: Y is T_0
( not Y is empty implies for x, y being Point of holds
( not x <> y or ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) ) )

proof

assume A11: not Y is empty ; :: thesis: for x, y being Point of holds
( not x <> y or ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) )
let x, y be Point of ; :: thesis: ( not x <> y or ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) )
assume A12: x <> y ; :: thesis: ( ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) )

hereby :: thesis: verum

per cases ( 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 ) ) by A10, A11, A12;

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

then consider E being Subset of such that
A13: E is closed and
A14: x in E and
A15: not y in E ;

now

take W = E ` ; :: thesis: ( W is open & not x in W & y in W )
W = ([#] Y) \ E ;
hence W is open by A13, PRE_TOPC:def 6; :: thesis: ( not x in W & y in W )
thus not x in W by A14, XBOOLE_0:def 5; :: thesis: y in W
thus y in W by A11, A15, SUBSET_1:50; :: thesis: verum

end;

hence ( ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) ) ; :: thesis: verum

end;

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

then consider F being Subset of such that
A16: F is closed and
A17: not x in F and
A18: y in F ;

now

take V = F ` ; :: thesis: ( V is open & x in V & not y in V )
V = ([#] Y) \ F ;
hence V is open by A16, PRE_TOPC:def 6; :: thesis: ( x in V & not y in V )
thus x in V by A11, A17, SUBSET_1:50; :: thesis: not y in V
thus not y in V by A18, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( ex V being Subset of st
( V is open & x in V & not y in V ) or ex W being Subset of st
( W is open & not x in W & y in W ) ) ; :: thesis: verum

end;

end;

end;

end;

hence Y is T_0 by Def3; :: thesis: verum