thus ( A is T_0 implies for x, y being Point of Y st x in A & y in A & 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: ( ( for x, y being Point of Y st x in A & y in A & 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 ) ) implies A is T_0 )

proof

assume A1: for x, y being Point of Y st x in A & y in A & 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 ) ; :: according to TSP_1:def 8 :: thesis: for x, y being Point of Y st x in A & y in A & 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 )
let x, y be Point of Y; :: thesis: ( x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) implies ex F being Subset of Y st
( F is closed & not x in F & y in F ) )
assume A2: ( x in A & y in A & x <> y ) ; :: thesis: ( 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 ) )

hereby :: thesis: verum

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

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

then consider V being Subset of Y such that
A3: V is open and
A4: x in V and
A5: 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 A3, PRE_TOPC:def 6; :: thesis: ( not x in F & y in F )
thus not x in F by A4, XBOOLE_0:def 5; :: thesis: y in F
thus y in F by A5, SUBSET_1:50; :: thesis: verum

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

end;

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

then consider W being Subset of Y such that
A6: W is open and
A7: not x in W and
A8: 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 A6, PRE_TOPC:def 6; :: thesis: ( x in E & not y in E )
thus x in E by A7, SUBSET_1:50; :: thesis: not y in E
thus not y in E by A8, XBOOLE_0:def 5; :: thesis: verum

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

end;

end;

end;

end;

assume A9: for x, y being Point of Y st x in A & y in A & 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: A is T_0
for x, y being Point of Y st x in A & y in A & 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 )

proof

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

hereby :: thesis: verum

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

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

then consider E being Subset of Y such that
A11: E is closed and
A12: x in E and
A13: 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 A11, PRE_TOPC:def 6; :: thesis: ( not x in W & y in W )
thus not x in W by A12, XBOOLE_0:def 5; :: thesis: y in W
thus y in W by A13, SUBSET_1:50; :: thesis: verum

end;

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

end;

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

then consider F being Subset of Y such that
A14: F is closed and
A15: not x in F and
A16: 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 A14, PRE_TOPC:def 6; :: thesis: ( x in V & not y in V )
thus x in V by A15, SUBSET_1:50; :: thesis: not y in V
thus not y in V by A16, XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

end;

end;

end;

hence A is T_0 by Def8; :: thesis: verum