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 )
proof
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 ) )
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, 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 ) )
then consider V being Subset of Y such that
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 )
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;
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
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 )
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;
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 A10: ( 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 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
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 ) )
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 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 ) )
then consider E being Subset of Y such that
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 )
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;
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
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 )
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;
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 Y is T_0 ; :: thesis: verum