thus
( not Y is T_0 or Y is empty or for x, y being Point of Y holds

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

( not x <> y or 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 ) ) ) implies Y is T_0 )

( not x <> y or 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: Y is T_0

( not Y is empty implies for x, y being Point of Y holds

( not x <> y or 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 ) ) )

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

( not x <> y or 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 ) ) ) implies Y is T_0 )

proof

assume A10:
( Y is empty or for x, y being Point of Y holds
assume A1:
( Y is empty or for x, y being Point of Y holds

( not x <> y or 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 ) ) ) ; :: according to TSP_1:def 3 :: thesis: ( Y is empty or for x, y being Point of Y holds

( not x <> y or 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 ) ) )

assume A2: not Y is empty ; :: thesis: for x, y being Point of Y holds

( not x <> y or 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 ) )

let x, y be Point of Y; :: thesis: ( not x <> y or 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 ) )

assume A3: 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 ) )

end;( not x <> y or 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 ) ) ) ; :: according to TSP_1:def 3 :: thesis: ( Y is empty or for x, y being Point of Y holds

( not x <> y or 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 ) ) )

assume A2: not Y is empty ; :: thesis: for x, y being Point of Y holds

( not x <> y or 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 ) )

let x, y be Point of Y; :: thesis: ( not x <> y or 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 ) )

assume A3: 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
end;

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, A3;

end;

( 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, A3;

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 ) )

( 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

A4: V is open and

A5: x in V and

A6: not y in V ;

( 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;A4: V is open and

A5: x in V and

A6: not y in V ;

now :: thesis: ex F being Element of K19( the carrier of Y) st

( F is closed & not x in F & y in F )

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

take F = V ` ; :: thesis: ( F is closed & not x in F & y in F )

V = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A4, PRE_TOPC:def 3; :: 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:29; :: thesis: verum

end;V = ([#] Y) \ F by PRE_TOPC:3;

hence F is closed by A4, PRE_TOPC:def 3; :: 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:29; :: thesis: verum

( 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

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 ) )

( 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

A7: W is open and

A8: not x in W and

A9: y in W ;

( 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;A7: W is open and

A8: not x in W and

A9: y in W ;

now :: thesis: ex E being Element of K19( the carrier of Y) st

( E is closed & x in E & not y in E )

hence
( ex E being Subset of Y st ( E is closed & x in E & not y in E )

take E = W ` ; :: thesis: ( E is closed & x in E & not y in E )

W = ([#] Y) \ E by PRE_TOPC:3;

hence E is closed by A7, PRE_TOPC:def 3; :: thesis: ( x in E & not y in E )

thus x in E by A2, A8, SUBSET_1:29; :: thesis: not y in E

thus not y in E by A9, XBOOLE_0:def 5; :: thesis: verum

end;W = ([#] Y) \ E by PRE_TOPC:3;

hence E is closed by A7, PRE_TOPC:def 3; :: thesis: ( x in E & not y in E )

thus x in E by A2, A8, SUBSET_1:29; :: thesis: not y in E

thus not y in E by A9, XBOOLE_0:def 5; :: thesis: verum

( 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

( not x <> y or 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: Y is T_0

( not Y is empty implies for x, y being Point of Y holds

( not x <> y or 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 ) ) )

proof

hence
Y is T_0
; :: thesis: verum
assume A11:
not Y is empty
; :: thesis: for x, y being Point of Y holds

( not x <> y or 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 ) )

let x, y be Point of Y; :: thesis: ( not x <> y or 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 ) )

assume A12: 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 ) )

end;( not x <> y or 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 ) )

let x, y be Point of Y; :: thesis: ( not x <> y or 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 ) )

assume A12: 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
end;

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 A10, A11, A12;

end;

( 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 A10, A11, A12;

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 ) )

( 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

A13: E is closed and

A14: x in E and

A15: not y in E ;

( 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;A13: E is closed and

A14: x in E and

A15: not y in E ;

now :: thesis: ex W being Element of K19( the carrier of Y) st

( W is open & not x in W & y in W )

hence
( ex V being Subset of Y st ( W is open & not x in W & y in W )

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 3; :: 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:29; :: thesis: verum

end;W = ([#] Y) \ E ;

hence W is open by A13, PRE_TOPC:def 3; :: 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:29; :: thesis: verum

( 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

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 ) )

( 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

A16: F is closed and

A17: not x in F and

A18: y in F ;

( 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;A16: F is closed and

A17: not x in F and

A18: y in F ;

now :: thesis: ex V being Element of K19( the carrier of Y) st

( V is open & x in V & not y in V )

hence
( ex V being Subset of Y st ( V is open & x in V & not y in V )

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 3; :: thesis: ( x in V & not y in V )

thus x in V by A11, A17, SUBSET_1:29; :: thesis: not y in V

thus not y in V by A18, XBOOLE_0:def 5; :: thesis: verum

end;V = ([#] Y) \ F ;

hence V is open by A16, PRE_TOPC:def 3; :: thesis: ( x in V & not y in V )

thus x in V by A11, A17, SUBSET_1:29; :: thesis: not y in V

thus not y in V by A18, XBOOLE_0:def 5; :: thesis: verum

( 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