:: TSP_1 semantic presentation begin definition let Y be TopStruct ; redefine mode SubSpace of Y means :Def1: :: TSP_1:def 1 ( the carrier of it c= the carrier of Y & ( for G0 being Subset of it holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of it ) ) ) ); compatibility for b1 being TopStruct holds ( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for G0 being Subset of b1 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of b1 ) ) ) ) ) proof let Y0 be TopStruct ; ::_thesis: ( Y0 is SubSpace of Y iff ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) ) A1: ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ; thus ( Y0 is SubSpace of Y implies ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) ) ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ) implies Y0 is SubSpace of Y ) proof assume A2: Y0 is SubSpace of Y ; ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ) ) hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def_4; ::_thesis: for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) thus for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: verum proof let G0 be Subset of Y0; ::_thesis: ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) thus ( G0 is open implies ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: ( ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) implies G0 is open ) proof assume G0 is open ; ::_thesis: ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) then G0 in the topology of Y0 by PRE_TOPC:def_2; then consider G being Subset of Y such that A3: G in the topology of Y and A4: G0 = G /\ ([#] Y0) by A2, PRE_TOPC:def_4; reconsider G = G as Subset of Y ; take G ; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 ) thus G is open by A3, PRE_TOPC:def_2; ::_thesis: G0 = G /\ the carrier of Y0 thus G0 = G /\ the carrier of Y0 by A4; ::_thesis: verum end; given G being Subset of Y such that A5: G is open and A6: G0 = G /\ the carrier of Y0 ; ::_thesis: G0 is open now__::_thesis:_ex_G_being_Subset_of_Y_st_ (_G_in_the_topology_of_Y_&_G0_=_G_/\_([#]_Y0)_) take G = G; ::_thesis: ( G in the topology of Y & G0 = G /\ ([#] Y0) ) thus G in the topology of Y by A5, PRE_TOPC:def_2; ::_thesis: G0 = G /\ ([#] Y0) thus G0 = G /\ ([#] Y0) by A6; ::_thesis: verum end; then G0 in the topology of Y0 by A2, PRE_TOPC:def_4; hence G0 is open by PRE_TOPC:def_2; ::_thesis: verum end; end; assume that A7: the carrier of Y0 c= the carrier of Y and A8: for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ; ::_thesis: Y0 is SubSpace of Y A9: for G0 being Subset of Y0 holds ( G0 in the topology of Y0 iff ex G being Subset of Y st ( G in the topology of Y & G0 = G /\ ([#] Y0) ) ) proof let G0 be Subset of Y0; ::_thesis: ( G0 in the topology of Y0 iff ex G being Subset of Y st ( G in the topology of Y & G0 = G /\ ([#] Y0) ) ) reconsider M = G0 as Subset of Y0 ; thus ( G0 in the topology of Y0 implies ex G being Subset of Y st ( G in the topology of Y & G0 = G /\ ([#] Y0) ) ) ::_thesis: ( ex G being Subset of Y st ( G in the topology of Y & G0 = G /\ ([#] Y0) ) implies G0 in the topology of Y0 ) proof reconsider M = G0 as Subset of Y0 ; assume G0 in the topology of Y0 ; ::_thesis: ex G being Subset of Y st ( G in the topology of Y & G0 = G /\ ([#] Y0) ) then M is open by PRE_TOPC:def_2; then consider G being Subset of Y such that A10: G is open and A11: G0 = G /\ the carrier of Y0 by A8; take G ; ::_thesis: ( G in the topology of Y & G0 = G /\ ([#] Y0) ) thus G in the topology of Y by A10, PRE_TOPC:def_2; ::_thesis: G0 = G /\ ([#] Y0) thus G0 = G /\ ([#] Y0) by A11; ::_thesis: verum end; given G being Subset of Y such that A12: G in the topology of Y and A13: G0 = G /\ ([#] Y0) ; ::_thesis: G0 in the topology of Y0 reconsider G = G as Subset of Y ; now__::_thesis:_ex_G_being_Subset_of_Y_st_ (_G_is_open_&_G0_=_G_/\_the_carrier_of_Y0_) take G = G; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 ) thus G is open by A12, PRE_TOPC:def_2; ::_thesis: G0 = G /\ the carrier of Y0 thus G0 = G /\ the carrier of Y0 by A13; ::_thesis: verum end; then M is open by A8; hence G0 in the topology of Y0 by PRE_TOPC:def_2; ::_thesis: verum end; [#] Y0 c= [#] Y by A7; hence Y0 is SubSpace of Y by A9, PRE_TOPC:def_4; ::_thesis: verum end; end; :: deftheorem Def1 defines SubSpace TSP_1:def_1_:_ for Y, b2 being TopStruct holds ( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for G0 being Subset of b2 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of b2 ) ) ) ) ); theorem Th1: :: TSP_1:1 for Y being TopStruct for Y0 being SubSpace of Y for G being Subset of Y st G is open holds ex G0 being Subset of Y0 st ( G0 is open & G0 = G /\ the carrier of Y0 ) proof let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y for G being Subset of Y st G is open holds ex G0 being Subset of Y0 st ( G0 is open & G0 = G /\ the carrier of Y0 ) let Y0 be SubSpace of Y; ::_thesis: for G being Subset of Y st G is open holds ex G0 being Subset of Y0 st ( G0 is open & G0 = G /\ the carrier of Y0 ) let G be Subset of Y; ::_thesis: ( G is open implies ex G0 being Subset of Y0 st ( G0 is open & G0 = G /\ the carrier of Y0 ) ) assume A1: G is open ; ::_thesis: ex G0 being Subset of Y0 st ( G0 is open & G0 = G /\ the carrier of Y0 ) ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ; then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def_4; reconsider G0 = G /\ A as Subset of Y0 by XBOOLE_1:17; take G0 ; ::_thesis: ( G0 is open & G0 = G /\ the carrier of Y0 ) thus G0 is open by A1, Def1; ::_thesis: G0 = G /\ the carrier of Y0 thus G0 = G /\ the carrier of Y0 ; ::_thesis: verum end; definition let Y be TopStruct ; redefine mode SubSpace of Y means :Def2: :: TSP_1:def 2 ( the carrier of it c= the carrier of Y & ( for F0 being Subset of it holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of it ) ) ) ); compatibility for b1 being TopStruct holds ( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for F0 being Subset of b1 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of b1 ) ) ) ) ) proof let Y0 be TopStruct ; ::_thesis: ( Y0 is SubSpace of Y iff ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) ) A1: ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ; thus ( Y0 is SubSpace of Y implies ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) ) ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ) implies Y0 is SubSpace of Y ) proof assume A2: Y0 is SubSpace of Y ; ::_thesis: ( the carrier of Y0 c= the carrier of Y & ( for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ) ) hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def_4; ::_thesis: for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) [#] Y0 c= [#] Y by A2, PRE_TOPC:def_4; then A3: ([#] Y0) \ ([#] Y) = {} by XBOOLE_1:37; thus for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ::_thesis: verum proof let F0 be Subset of Y0; ::_thesis: ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) set G0 = ([#] Y0) \ F0; thus ( F0 is closed implies ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ::_thesis: ( ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) implies F0 is closed ) proof assume F0 is closed ; ::_thesis: ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) then ([#] Y0) \ F0 is open by PRE_TOPC:def_3; then consider G being Subset of Y such that A4: G is open and A5: ([#] Y0) \ F0 = G /\ the carrier of Y0 by A2, Def1; take F = ([#] Y) \ G; ::_thesis: ( F is closed & F0 = F /\ the carrier of Y0 ) A6: G = ([#] Y) \ F by PRE_TOPC:3; hence F is closed by A4, PRE_TOPC:def_3; ::_thesis: F0 = F /\ the carrier of Y0 F0 = ([#] Y0) \ (G /\ the carrier of Y0) by A5, PRE_TOPC:3 .= (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by XBOOLE_1:54 .= (([#] Y0) \ G) \/ {} by XBOOLE_1:37 .= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A6, XBOOLE_1:52 .= ([#] Y0) /\ F by A3 ; hence F0 = F /\ the carrier of Y0 ; ::_thesis: verum end; given F being Subset of Y such that A7: F is closed and A8: F0 = F /\ the carrier of Y0 ; ::_thesis: F0 is closed now__::_thesis:_ex_G_being_Element_of_K19(_the_carrier_of_Y)_st_ (_G_is_open_&_([#]_Y0)_\_F0_=_G_/\_the_carrier_of_Y0_) take G = ([#] Y) \ F; ::_thesis: ( G is open & ([#] Y0) \ F0 = G /\ the carrier of Y0 ) A9: F = ([#] Y) \ G by PRE_TOPC:3; thus G is open by A7, PRE_TOPC:def_3; ::_thesis: ([#] Y0) \ F0 = G /\ the carrier of Y0 ([#] Y0) \ F0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A8, XBOOLE_1:54 .= (([#] Y0) \ F) \/ {} by XBOOLE_1:37 .= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A9, XBOOLE_1:52 .= ([#] Y0) /\ G by A3 ; hence ([#] Y0) \ F0 = G /\ the carrier of Y0 ; ::_thesis: verum end; then ([#] Y0) \ F0 is open by A2, Def1; hence F0 is closed by PRE_TOPC:def_3; ::_thesis: verum end; end; assume that A10: the carrier of Y0 c= the carrier of Y and A11: for F0 being Subset of Y0 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of Y0 ) ) ; ::_thesis: Y0 is SubSpace of Y A12: ([#] Y0) \ ([#] Y) = {} by A10, XBOOLE_1:37; for G0 being Subset of Y0 holds ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) proof let G0 be Subset of Y0; ::_thesis: ( G0 is open iff ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) set F0 = ([#] Y0) \ G0; thus ( G0 is open implies ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) ) ::_thesis: ( ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) implies G0 is open ) proof set F0 = ([#] Y0) \ G0; A13: G0 = ([#] Y0) \ (([#] Y0) \ G0) by PRE_TOPC:3; assume G0 is open ; ::_thesis: ex G being Subset of Y st ( G is open & G0 = G /\ the carrier of Y0 ) then ([#] Y0) \ G0 is closed by A13, PRE_TOPC:def_3; then consider F being Subset of Y such that A14: F is closed and A15: ([#] Y0) \ G0 = F /\ the carrier of Y0 by A11; take G = ([#] Y) \ F; ::_thesis: ( G is open & G0 = G /\ the carrier of Y0 ) thus G is open by A14, PRE_TOPC:def_3; ::_thesis: G0 = G /\ the carrier of Y0 A16: F = ([#] Y) \ G by PRE_TOPC:3; G0 = (([#] Y0) \ F) \/ (([#] Y0) \ the carrier of Y0) by A13, A15, XBOOLE_1:54 .= (([#] Y0) \ F) \/ {} by XBOOLE_1:37 .= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ G) by A16, XBOOLE_1:52 .= ([#] Y0) /\ G by A12 ; hence G0 = G /\ the carrier of Y0 ; ::_thesis: verum end; given G being Subset of Y such that A17: G is open and A18: G0 = G /\ the carrier of Y0 ; ::_thesis: G0 is open now__::_thesis:_ex_F_being_Element_of_K19(_the_carrier_of_Y)_st_ (_F_is_closed_&_([#]_Y0)_\_G0_=_F_/\_the_carrier_of_Y0_) take F = ([#] Y) \ G; ::_thesis: ( F is closed & ([#] Y0) \ G0 = F /\ the carrier of Y0 ) A19: G = ([#] Y) \ F by PRE_TOPC:3; hence F is closed by A17, PRE_TOPC:def_3; ::_thesis: ([#] Y0) \ G0 = F /\ the carrier of Y0 ([#] Y0) \ G0 = (([#] Y0) \ G) \/ (([#] Y0) \ the carrier of Y0) by A18, XBOOLE_1:54 .= (([#] Y0) \ G) \/ {} by XBOOLE_1:37 .= (([#] Y0) \ ([#] Y)) \/ (([#] Y0) /\ F) by A19, XBOOLE_1:52 .= ([#] Y0) /\ F by A12 ; hence ([#] Y0) \ G0 = F /\ the carrier of Y0 ; ::_thesis: verum end; then ( G0 = ([#] Y0) \ (([#] Y0) \ G0) & ([#] Y0) \ G0 is closed ) by A11, PRE_TOPC:3; hence G0 is open by PRE_TOPC:def_3; ::_thesis: verum end; hence Y0 is SubSpace of Y by A10, Def1; ::_thesis: verum end; end; :: deftheorem Def2 defines SubSpace TSP_1:def_2_:_ for Y, b2 being TopStruct holds ( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for F0 being Subset of b2 holds ( F0 is closed iff ex F being Subset of Y st ( F is closed & F0 = F /\ the carrier of b2 ) ) ) ) ); theorem Th2: :: TSP_1:2 for Y being TopStruct for Y0 being SubSpace of Y for F being Subset of Y st F is closed holds ex F0 being Subset of Y0 st ( F0 is closed & F0 = F /\ the carrier of Y0 ) proof let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y for F being Subset of Y st F is closed holds ex F0 being Subset of Y0 st ( F0 is closed & F0 = F /\ the carrier of Y0 ) let Y0 be SubSpace of Y; ::_thesis: for F being Subset of Y st F is closed holds ex F0 being Subset of Y0 st ( F0 is closed & F0 = F /\ the carrier of Y0 ) let F be Subset of Y; ::_thesis: ( F is closed implies ex F0 being Subset of Y0 st ( F0 is closed & F0 = F /\ the carrier of Y0 ) ) assume A1: F is closed ; ::_thesis: ex F0 being Subset of Y0 st ( F0 is closed & F0 = F /\ the carrier of Y0 ) ( [#] Y0 = the carrier of Y0 & [#] Y = the carrier of Y ) ; then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def_4; reconsider F0 = F /\ A as Subset of Y0 by XBOOLE_1:17; take F0 ; ::_thesis: ( F0 is closed & F0 = F /\ the carrier of Y0 ) thus F0 is closed by A1, Def2; ::_thesis: F0 = F /\ the carrier of Y0 thus F0 = F /\ the carrier of Y0 ; ::_thesis: verum end; begin definition let T be TopStruct ; redefine attr T is T_0 means :Def3: :: TSP_1:def 3 ( T is empty or for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ); compatibility ( T is T_0 iff ( T is empty or for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ) ) proof hereby ::_thesis: ( ( T is empty or for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ) implies T is T_0 ) assume A1: T is T_0 ; ::_thesis: ( not T is empty implies for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ) assume A2: not T is empty ; ::_thesis: for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) let x, y be Point of T; ::_thesis: ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) assume x <> y ; ::_thesis: ( ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) then ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A1, A2, T_0TOPSP:def_7; hence ( ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ; ::_thesis: verum end; assume A3: ( T is empty or for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ) ; ::_thesis: T is T_0 assume A4: not T is empty ; :: according to T_0TOPSP:def_7 ::_thesis: for b1, b2 being Element of the carrier of T holds ( b1 = b2 or ex b3 being Element of K19( the carrier of T) st ( b3 is open & ( ( b1 in b3 & not b2 in b3 ) or ( b2 in b3 & not b1 in b3 ) ) ) ) let x, y be Point of T; ::_thesis: ( x = y or ex b1 being Element of K19( the carrier of T) st ( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) ) assume x <> y ; ::_thesis: ex b1 being Element of K19( the carrier of T) st ( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) then ( ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) by A3, A4; hence ex b1 being Element of K19( the carrier of T) st ( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def3 defines T_0 TSP_1:def_3_:_ for T being TopStruct holds ( T is T_0 iff ( T is empty or for x, y being Point of T holds ( not x <> y or ex V being Subset of T st ( V is open & x in V & not y in V ) or ex W being Subset of T st ( W is open & not x in W & y in W ) ) ) ); definition let Y be TopStruct ; redefine attr Y is T_0 means :Def4: :: TSP_1:def 4 ( 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 ) ) ); compatibility ( Y is T_0 iff ( 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 ) ) ) ) proof 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 percases ( 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 percases ( 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 by Def3; ::_thesis: verum end; end; :: deftheorem Def4 defines T_0 TSP_1:def_4_:_ for Y being TopStruct holds ( Y is T_0 iff ( 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 ) ) ) ); registration cluster non empty trivial -> non empty T_0 for TopStruct ; coherence for b1 being non empty TopStruct st b1 is trivial holds b1 is T_0 proof let Y be non empty TopStruct ; ::_thesis: ( Y is trivial implies Y is T_0 ) assume Y is trivial ; ::_thesis: Y is T_0 then consider a being Point of Y such that A1: the carrier of Y = {a} by TEX_1:def_1; now__::_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 A2: 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 ) ) x = a by A1, TARSKI:def_1; 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 ) ) by A1, A2, TARSKI:def_1; ::_thesis: verum end; hence Y is T_0 by Def3; ::_thesis: verum end; end; Lm1: for X being non trivial anti-discrete TopStruct holds not X is T_0 proof let X be non trivial anti-discrete TopStruct ; ::_thesis: not X is T_0 now__::_thesis:_ex_x,_y_being_Point_of_X_st_ (_x_<>_y_&_(_for_V_being_Subset_of_X_holds_ (_not_V_is_open_or_not_x_in_V_or_y_in_V_)_)_&_(_for_W_being_Subset_of_X_holds_ (_not_W_is_open_or_x_in_W_or_not_y_in_W_)_)_) consider x, y being Point of X such that A1: x <> y by STRUCT_0:def_10; take x = x; ::_thesis: ex y being Point of X st ( x <> y & ( for V being Subset of X holds ( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds ( not W is open or x in W or not y in W ) ) ) take y = y; ::_thesis: ( x <> y & ( for V being Subset of X holds ( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds ( not W is open or x in W or not y in W ) ) ) thus x <> y by A1; ::_thesis: ( ( for V being Subset of X holds ( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds ( not W is open or x in W or not y in W ) ) ) A2: now__::_thesis:_for_V_being_Subset_of_X_st_V_is_open_&_y_in_V_holds_ x_in_V let V be Subset of X; ::_thesis: ( V is open & y in V implies x in V ) assume V is open ; ::_thesis: ( y in V implies x in V ) then A3: ( V = {} or V = the carrier of X ) by TDLAT_3:18; assume y in V ; ::_thesis: x in V hence x in V by A3; ::_thesis: verum end; now__::_thesis:_for_V_being_Subset_of_X_st_V_is_open_&_x_in_V_holds_ y_in_V let V be Subset of X; ::_thesis: ( V is open & x in V implies y in V ) assume V is open ; ::_thesis: ( x in V implies y in V ) then A4: ( V = {} or V = the carrier of X ) by TDLAT_3:18; assume x in V ; ::_thesis: y in V hence y in V by A4; ::_thesis: verum end; hence ( ( for V being Subset of X holds ( not V is open or not x in V or y in V ) ) & ( for W being Subset of X holds ( not W is open or x in W or not y in W ) ) ) by A2; ::_thesis: verum end; hence not X is T_0 by Def3; ::_thesis: verum end; registration cluster non empty strict TopSpace-like T_0 for TopStruct ; existence ex b1 being TopSpace st ( b1 is strict & b1 is T_0 & not b1 is empty ) proof set X = the non empty trivial strict TopSpace; take the non empty trivial strict TopSpace ; ::_thesis: ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty ) thus ( the non empty trivial strict TopSpace is strict & the non empty trivial strict TopSpace is T_0 & not the non empty trivial strict TopSpace is empty ) ; ::_thesis: verum end; cluster non empty strict TopSpace-like non T_0 for TopStruct ; existence ex b1 being TopSpace st ( b1 is strict & not b1 is T_0 & not b1 is empty ) proof set X = the non empty non trivial strict anti-discrete TopSpace; take the non empty non trivial strict anti-discrete TopSpace ; ::_thesis: ( the non empty non trivial strict anti-discrete TopSpace is strict & not the non empty non trivial strict anti-discrete TopSpace is T_0 & not the non empty non trivial strict anti-discrete TopSpace is empty ) thus ( the non empty non trivial strict anti-discrete TopSpace is strict & not the non empty non trivial strict anti-discrete TopSpace is T_0 & not the non empty non trivial strict anti-discrete TopSpace is empty ) by Lm1; ::_thesis: verum end; end; registration cluster non empty TopSpace-like discrete -> non empty T_0 for TopStruct ; coherence for b1 being non empty TopSpace st b1 is discrete holds b1 is T_0 proof let Y be non empty TopSpace; ::_thesis: ( Y is discrete implies Y is T_0 ) assume A1: Y is discrete ; ::_thesis: Y is T_0 now__::_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 A2: 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 ) ) 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 = {x}; ::_thesis: ( V is open & x in V & not y in V ) thus V is open by A1, TDLAT_3:15; ::_thesis: ( x in V & not y in V ) thus x in V by TARSKI:def_1; ::_thesis: not y in V thus not y in V by A2, TARSKI:def_1; ::_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; hence Y is T_0 by Def3; ::_thesis: verum end; cluster non empty TopSpace-like non T_0 -> non empty non discrete for TopStruct ; coherence for b1 being non empty TopSpace st not b1 is T_0 holds not b1 is discrete ; cluster non empty non trivial TopSpace-like anti-discrete -> non empty non T_0 for TopStruct ; coherence for b1 being non empty TopSpace st b1 is anti-discrete & not b1 is trivial holds not b1 is T_0 by Lm1; cluster non empty TopSpace-like T_0 anti-discrete -> non empty trivial for TopStruct ; coherence for b1 being non empty TopSpace st b1 is anti-discrete & b1 is T_0 holds b1 is trivial ; cluster non empty non trivial TopSpace-like T_0 -> non empty non anti-discrete for TopStruct ; coherence for b1 being non empty TopSpace st b1 is T_0 & not b1 is trivial holds not b1 is anti-discrete ; end; Lm2: for X being non empty TopSpace for x being Point of X holds x in Cl {x} proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds x in Cl {x} let x be Point of X; ::_thesis: x in Cl {x} ( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1; hence x in Cl {x} ; ::_thesis: verum end; definition let X be non empty TopSpace; redefine attr X is T_0 means :Def5: :: TSP_1:def 5 for x, y being Point of X st x <> y holds Cl {x} <> Cl {y}; compatibility ( X is T_0 iff for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} ) proof thus ( X is T_0 implies for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} ) implies X is T_0 ) proof assume A1: X is T_0 ; ::_thesis: for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} ) assume A2: x <> y ; ::_thesis: Cl {x} <> Cl {y} now__::_thesis:_not_Cl_{x}_=_Cl_{y} percases ( ex V being Subset of X st ( V is open & x in V & not y in V ) or ex W being Subset of X st ( W is open & not x in W & y in W ) ) by A1, A2, Def3; suppose ex V being Subset of X st ( V is open & x in V & not y in V ) ; ::_thesis: not Cl {x} = Cl {y} then consider V being Subset of X such that A3: V is open and A4: x in V and A5: not y in V ; ( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1; then A6: (Cl {x}) /\ V <> {} by A4, XBOOLE_0:def_4; y in V ` by A5, SUBSET_1:29; then {y} c= V ` by ZFMISC_1:31; then {y} misses V by SUBSET_1:23; then A7: Cl {y} misses V by A3, TSEP_1:36; assume Cl {x} = Cl {y} ; ::_thesis: contradiction hence contradiction by A7, A6, XBOOLE_0:def_7; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & not x in W & y in W ) ; ::_thesis: not Cl {x} = Cl {y} then consider W being Subset of X such that A8: W is open and A9: not x in W and A10: y in W ; ( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def_1; then A11: (Cl {y}) /\ W <> {} by A10, XBOOLE_0:def_4; x in W ` by A9, SUBSET_1:29; then {x} c= W ` by ZFMISC_1:31; then {x} misses W by SUBSET_1:23; then A12: Cl {x} misses W by A8, TSEP_1:36; assume Cl {x} = Cl {y} ; ::_thesis: contradiction hence contradiction by A12, A11, XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence Cl {x} <> Cl {y} ; ::_thesis: verum end; end; assume A13: for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} ; ::_thesis: X is T_0 now__::_thesis:_for_x,_y_being_Point_of_X_st_x_<>_y_&_(_for_E_being_Subset_of_X_st_E_is_closed_&_x_in_E_holds_ y_in_E_)_holds_ ex_F_being_Subset_of_X_st_ (_F_is_closed_&_not_x_in_F_&_y_in_F_) let x, y be Point of X; ::_thesis: ( x <> y & ( for E being Subset of X st E is closed & x in E holds y in E ) implies ex F being Subset of X st ( F is closed & not x in F & y in F ) ) assume A14: x <> y ; ::_thesis: ( ( for E being Subset of X st E is closed & x in E holds y in E ) implies ex F being Subset of X st ( F is closed & not x in F & y in F ) ) assume A15: for E being Subset of X st E is closed & x in E holds y in E ; ::_thesis: ex F being Subset of X st ( F is closed & not x in F & y in F ) thus ex F being Subset of X st ( F is closed & not x in F & y in F ) ::_thesis: verum proof set F = Cl {y}; take Cl {y} ; ::_thesis: ( Cl {y} is closed & not x in Cl {y} & y in Cl {y} ) thus Cl {y} is closed ; ::_thesis: ( not x in Cl {y} & y in Cl {y} ) now__::_thesis:_not_x_in_Cl_{y} assume x in Cl {y} ; ::_thesis: contradiction then {x} c= Cl {y} by ZFMISC_1:31; then A16: Cl {x} c= Cl {y} by TOPS_1:5; y in Cl {x} by A15, Lm2; then {y} c= Cl {x} by ZFMISC_1:31; then Cl {y} c= Cl {x} by TOPS_1:5; then Cl {x} = Cl {y} by A16, XBOOLE_0:def_10; hence contradiction by A13, A14; ::_thesis: verum end; hence not x in Cl {y} ; ::_thesis: y in Cl {y} thus y in Cl {y} by Lm2; ::_thesis: verum end; end; hence X is T_0 by Def4; ::_thesis: verum end; end; :: deftheorem Def5 defines T_0 TSP_1:def_5_:_ for X being non empty TopSpace holds ( X is T_0 iff for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} ); definition let X be non empty TopSpace; redefine attr X is T_0 means :Def6: :: TSP_1:def 6 for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ); compatibility ( X is T_0 iff for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) proof thus ( X is T_0 implies for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) ::_thesis: ( ( for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) implies X is T_0 ) proof assume A1: X is T_0 ; ::_thesis: for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} ) assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} ) assume that A3: x in Cl {y} and A4: y in Cl {x} ; ::_thesis: contradiction {y} c= Cl {x} by A4, ZFMISC_1:31; then A5: Cl {y} c= Cl {x} by TOPS_1:5; {x} c= Cl {y} by A3, ZFMISC_1:31; then Cl {x} c= Cl {y} by TOPS_1:5; then Cl {x} = Cl {y} by A5, XBOOLE_0:def_10; hence contradiction by A1, A2, Def5; ::_thesis: verum end; end; assume A6: for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) ; ::_thesis: X is T_0 for x, y being Point of X st x <> y holds Cl {x} <> Cl {y} proof let x, y be Point of X; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} ) assume A7: x <> y ; ::_thesis: Cl {x} <> Cl {y} assume A8: Cl {x} = Cl {y} ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( not x in Cl {y} or not y in Cl {x} ) by A6, A7; suppose not x in Cl {y} ; ::_thesis: contradiction hence contradiction by A8, Lm2; ::_thesis: verum end; suppose not y in Cl {x} ; ::_thesis: contradiction hence contradiction by A8, Lm2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence X is T_0 by Def5; ::_thesis: verum end; end; :: deftheorem Def6 defines T_0 TSP_1:def_6_:_ for X being non empty TopSpace holds ( X is T_0 iff for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) ); definition let X be non empty TopSpace; redefine attr X is T_0 means :: TSP_1:def 7 for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x}; compatibility ( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) proof thus ( X is T_0 implies for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) implies X is T_0 ) proof assume A1: X is T_0 ; ::_thesis: for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x <> y & x in Cl {y} implies not Cl {y} c= Cl {x} ) assume A2: x <> y ; ::_thesis: ( x in Cl {y} implies not Cl {y} c= Cl {x} ) assume x in Cl {y} ; ::_thesis: not Cl {y} c= Cl {x} then {x} c= Cl {y} by ZFMISC_1:31; then A3: Cl {x} c= Cl {y} by TOPS_1:5; assume Cl {y} c= Cl {x} ; ::_thesis: contradiction then Cl {x} = Cl {y} by A3, XBOOLE_0:def_10; hence contradiction by A1, A2, Def5; ::_thesis: verum end; end; assume A4: for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ; ::_thesis: X is T_0 for x, y being Point of X holds ( not x <> y or not x in Cl {y} or not y in Cl {x} ) proof let x, y be Point of X; ::_thesis: ( not x <> y or not x in Cl {y} or not y in Cl {x} ) assume A5: x <> y ; ::_thesis: ( not x in Cl {y} or not y in Cl {x} ) assume A6: x in Cl {y} ; ::_thesis: not y in Cl {x} assume y in Cl {x} ; ::_thesis: contradiction then {y} c= Cl {x} by ZFMISC_1:31; hence contradiction by A4, A5, A6, TOPS_1:5; ::_thesis: verum end; hence X is T_0 by Def6; ::_thesis: verum end; end; :: deftheorem defines T_0 TSP_1:def_7_:_ for X being non empty TopSpace holds ( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ); registration cluster non empty TopSpace-like T_0 almost_discrete -> non empty discrete for TopStruct ; coherence for b1 being non empty TopSpace st b1 is almost_discrete & b1 is T_0 holds b1 is discrete proof let Y be non empty TopSpace; ::_thesis: ( Y is almost_discrete & Y is T_0 implies Y is discrete ) assume A1: ( Y is almost_discrete & Y is T_0 ) ; ::_thesis: Y is discrete for A being Subset of Y for x being Point of Y st A = {x} holds A is closed proof let A be Subset of Y; ::_thesis: for x being Point of Y st A = {x} holds A is closed let x be Point of Y; ::_thesis: ( A = {x} implies A is closed ) x in Cl {x} by Lm2; then A2: {x} c= Cl {x} by ZFMISC_1:31; A3: now__::_thesis:_Cl_{x}_c=_{x} assume not Cl {x} c= {x} ; ::_thesis: contradiction then consider a being set such that A4: a in Cl {x} and A5: not a in {x} by TARSKI:def_3; reconsider a = a as Point of Y by A4; a <> x by A5, TARSKI:def_1; then not x in Cl {a} by A1, A4, Def6; then x in (Cl {a}) ` by SUBSET_1:29; then {x} c= (Cl {a}) ` by ZFMISC_1:31; then A6: {x} misses Cl {a} by SUBSET_1:23; A7: ( a in {a} & {a} c= Cl {a} ) by PRE_TOPC:18, TARSKI:def_1; Cl {a} is open by A1, TDLAT_3:22; then Cl {x} misses Cl {a} by A6, TSEP_1:36; hence contradiction by A4, A7, XBOOLE_0:3; ::_thesis: verum end; assume A = {x} ; ::_thesis: A is closed hence A is closed by A2, A3, XBOOLE_0:def_10; ::_thesis: verum end; hence Y is discrete by A1, TDLAT_3:26; ::_thesis: verum end; cluster non empty TopSpace-like non discrete almost_discrete -> non empty non T_0 for TopStruct ; coherence for b1 being non empty TopSpace st b1 is almost_discrete & not b1 is discrete holds not b1 is T_0 ; cluster non empty TopSpace-like T_0 non discrete -> non empty non almost_discrete for TopStruct ; coherence for b1 being non empty TopSpace st not b1 is discrete & b1 is T_0 holds not b1 is almost_discrete ; end; definition mode Kolmogorov_space is non empty T_0 TopSpace; mode non-Kolmogorov_space is non empty non T_0 TopSpace; end; registration cluster non empty non trivial strict TopSpace-like T_0 for TopStruct ; existence ex b1 being Kolmogorov_space st ( not b1 is trivial & b1 is strict ) proof set X = the non empty non trivial strict discrete TopSpace; take the non empty non trivial strict discrete TopSpace ; ::_thesis: ( not the non empty non trivial strict discrete TopSpace is trivial & the non empty non trivial strict discrete TopSpace is strict ) thus ( not the non empty non trivial strict discrete TopSpace is trivial & the non empty non trivial strict discrete TopSpace is strict ) ; ::_thesis: verum end; cluster non empty non trivial strict TopSpace-like non T_0 non discrete for TopStruct ; existence ex b1 being non-Kolmogorov_space st ( not b1 is trivial & b1 is strict ) proof set X = the non empty non trivial strict anti-discrete TopSpace; take the non empty non trivial strict anti-discrete TopSpace ; ::_thesis: ( not the non empty non trivial strict anti-discrete TopSpace is trivial & the non empty non trivial strict anti-discrete TopSpace is strict ) thus ( not the non empty non trivial strict anti-discrete TopSpace is trivial & the non empty non trivial strict anti-discrete TopSpace is strict ) ; ::_thesis: verum end; end; begin definition let Y be TopStruct ; let IT be Subset of Y; attrIT is T_0 means :Def8: :: TSP_1:def 8 for x, y being Point of Y st x in IT & y in IT & 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 ); end; :: deftheorem Def8 defines T_0 TSP_1:def_8_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is T_0 iff for x, y being Point of Y st x in IT & y in IT & 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 ) ); definition let Y be non empty TopStruct ; let A be Subset of Y; redefine attr A is T_0 means :Def9: :: TSP_1:def 9 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 ); compatibility ( A is T_0 iff 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 ) ) proof 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 percases ( 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__::_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 A3, PRE_TOPC:def_3; ::_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: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 A6: W is open and A7: not x in W and A8: 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 A6, PRE_TOPC:def_3; ::_thesis: ( x in E & not y in E ) thus x in E by A7, SUBSET_1:29; ::_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 percases ( 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__::_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 A11, PRE_TOPC:def_3; ::_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: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 A14: F is closed and A15: not x in F and A16: 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 A14, PRE_TOPC:def_3; ::_thesis: ( x in V & not y in V ) thus x in V by A15, SUBSET_1:29; ::_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 end; end; :: deftheorem Def9 defines T_0 TSP_1:def_9_:_ for Y being non empty TopStruct for A being Subset of Y holds ( A is T_0 iff 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 ) ); theorem :: TSP_1:3 for Y0, Y1 being TopStruct for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds D1 is T_0 proof let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds D1 is T_0 let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds D1 is T_0 let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 implies D1 is T_0 ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is T_0 or D1 is T_0 ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is T_0 or D1 is T_0 ) assume A3: D0 is T_0 ; ::_thesis: D1 is T_0 now__::_thesis:_for_x,_y_being_Point_of_Y1_st_x_in_D1_&_y_in_D1_&_x_<>_y_&_(_for_V1_being_Subset_of_Y1_holds_ (_not_V1_is_open_or_not_x_in_V1_or_y_in_V1_)_)_holds_ ex_W1_being_Subset_of_Y1_st_ (_W1_is_open_&_not_x_in_W1_&_y_in_W1_) let x, y be Point of Y1; ::_thesis: ( x in D1 & y in D1 & x <> y & ( for V1 being Subset of Y1 holds ( not V1 is open or not x in V1 or y in V1 ) ) implies ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) reconsider x0 = x, y0 = y as Point of Y0 by A1; assume A4: ( x in D1 & y in D1 ) ; ::_thesis: ( not x <> y or ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) assume A5: x <> y ; ::_thesis: ( ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) hereby ::_thesis: verum percases ( ex V being Subset of Y0 st ( V is open & x0 in V & not y0 in V ) or ex W being Subset of Y0 st ( W is open & not x0 in W & y0 in W ) ) by A2, A3, A4, A5, Def8; suppose ex V being Subset of Y0 st ( V is open & x0 in V & not y0 in V ) ; ::_thesis: ( ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) then consider V being Subset of Y0 such that A6: V is open and A7: ( x0 in V & not y0 in V ) ; reconsider V1 = V as Subset of Y1 by A1; now__::_thesis:_ex_V1_being_Subset_of_Y1_st_ (_V1_is_open_&_x_in_V1_&_not_y_in_V1_) take V1 = V1; ::_thesis: ( V1 is open & x in V1 & not y in V1 ) V1 in the topology of Y1 by A1, A6, PRE_TOPC:def_2; hence V1 is open by PRE_TOPC:def_2; ::_thesis: ( x in V1 & not y in V1 ) thus ( x in V1 & not y in V1 ) by A7; ::_thesis: verum end; hence ( ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) ; ::_thesis: verum end; suppose ex W being Subset of Y0 st ( W is open & not x0 in W & y0 in W ) ; ::_thesis: ( ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) then consider W being Subset of Y0 such that A8: W is open and A9: ( not x0 in W & y0 in W ) ; reconsider W1 = W as Subset of Y1 by A1; now__::_thesis:_ex_W1_being_Subset_of_Y1_st_ (_W1_is_open_&_not_x_in_W1_&_y_in_W1_) take W1 = W1; ::_thesis: ( W1 is open & not x in W1 & y in W1 ) W1 in the topology of Y1 by A1, A8, PRE_TOPC:def_2; hence W1 is open by PRE_TOPC:def_2; ::_thesis: ( not x in W1 & y in W1 ) thus ( not x in W1 & y in W1 ) by A9; ::_thesis: verum end; hence ( ex V1 being Subset of Y1 st ( V1 is open & x in V1 & not y in V1 ) or ex W1 being Subset of Y1 st ( W1 is open & not x in W1 & y in W1 ) ) ; ::_thesis: verum end; end; end; end; hence D1 is T_0 by Def8; ::_thesis: verum end; theorem Th4: :: TSP_1:4 for Y being non empty TopStruct for A being Subset of Y st A = the carrier of Y holds ( A is T_0 iff Y is T_0 ) proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A = the carrier of Y holds ( A is T_0 iff Y is T_0 ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y implies ( A is T_0 iff Y is T_0 ) ) assume A1: A = the carrier of Y ; ::_thesis: ( A is T_0 iff Y is T_0 ) hereby ::_thesis: ( Y is T_0 implies A is T_0 ) assume A is T_0 ; ::_thesis: Y is T_0 then 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 ) ) by A1, Def8; hence Y is T_0 by Def3; ::_thesis: verum end; hereby ::_thesis: verum assume Y is T_0 ; ::_thesis: A is T_0 then 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 ) by Def3; hence A is T_0 by Def8; ::_thesis: verum end; end; theorem Th5: :: TSP_1:5 for Y being non empty TopStruct for A, B being Subset of Y st B c= A & A is T_0 holds B is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is T_0 holds B is T_0 let A, B be Subset of Y; ::_thesis: ( B c= A & A is T_0 implies B is T_0 ) assume A1: B c= A ; ::_thesis: ( not A is T_0 or B is T_0 ) assume A is T_0 ; ::_thesis: B is T_0 then for x, y being Point of Y st x in B & y in B & 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 ) by A1, Def8; hence B is T_0 by Def8; ::_thesis: verum end; theorem Th6: :: TSP_1:6 for Y being non empty TopStruct for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds A /\ B is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds A /\ B is T_0 let A, B be Subset of Y; ::_thesis: ( ( A is T_0 or B is T_0 ) implies A /\ B is T_0 ) assume A1: ( A is T_0 or B is T_0 ) ; ::_thesis: A /\ B is T_0 hereby ::_thesis: verum percases ( A is T_0 or B is T_0 ) by A1; suppose A is T_0 ; ::_thesis: A /\ B is T_0 hence A /\ B is T_0 by Th5, XBOOLE_1:17; ::_thesis: verum end; suppose B is T_0 ; ::_thesis: A /\ B is T_0 hence A /\ B is T_0 by Th5, XBOOLE_1:17; ::_thesis: verum end; end; end; end; theorem Th7: :: TSP_1:7 for Y being non empty TopStruct for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds A \/ B is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds A \/ B is T_0 let A, B be Subset of Y; ::_thesis: ( ( A is open or B is open ) & A is T_0 & B is T_0 implies A \/ B is T_0 ) assume A1: ( A is open or B is open ) ; ::_thesis: ( not A is T_0 or not B is T_0 or A \/ B is T_0 ) assume that A2: A is T_0 and A3: B is T_0 ; ::_thesis: A \/ B is T_0 now__::_thesis:_for_x,_y_being_Point_of_Y_st_x_in_A_\/_B_&_y_in_A_\/_B_&_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_) let x, y be Point of Y; ::_thesis: ( x in A \/ B & y in A \/ B & 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 A4: ( x in A \/ B & y in A \/ B ) ; ::_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 ) ) then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39; assume A6: 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 ) ) A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39; now__::_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_)_) percases ( A is open or B is open ) by A1; supposeA8: A is open ; ::_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 ) ) now__::_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_)_) percases ( ( x in A & y in A ) or ( x in A & y in B \ A ) or ( x in B \ A & y in A ) or ( x in B \ A & y in B \ A ) ) by A7, XBOOLE_0:def_3; suppose ( x in A & y in A ) ; ::_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 ) ) 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 ) ) by A2, A6, Def8; ::_thesis: verum end; supposeA9: ( x in A & y in B \ A ) ; ::_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 ) ) now__::_thesis:_ex_A_being_Subset_of_Y_st_ (_A_is_open_&_x_in_A_&_not_y_in_A_) take A = A; ::_thesis: ( A is open & x in A & not y in A ) thus A is open by A8; ::_thesis: ( x in A & not y in A ) thus x in A by A9; ::_thesis: not y in A thus not y in A by A9, 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; supposeA10: ( x in B \ A & y in A ) ; ::_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 ) ) now__::_thesis:_ex_A_being_Subset_of_Y_st_ (_A_is_open_&_not_x_in_A_&_y_in_A_) take A = A; ::_thesis: ( A is open & not x in A & y in A ) thus A is open by A8; ::_thesis: ( not x in A & y in A ) thus not x in A by A10, XBOOLE_0:def_5; ::_thesis: y in A thus y in A by A10; ::_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; supposeA11: ( x in B \ A & y in B \ A ) ; ::_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 ) ) B \ A c= B by XBOOLE_1:36; 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 ) ) by A3, A6, A11, Def8; ::_thesis: verum end; end; 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; supposeA12: B is open ; ::_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 ) ) now__::_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_)_) percases ( ( x in A \ B & y in A \ B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) or ( x in B & y in B ) ) by A5, XBOOLE_0:def_3; supposeA13: ( x in A \ B & y in A \ B ) ; ::_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 ) ) A \ B c= A by XBOOLE_1:36; 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 ) ) by A2, A6, A13, Def8; ::_thesis: verum end; supposeA14: ( x in A \ B & y in B ) ; ::_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 ) ) now__::_thesis:_ex_B_being_Subset_of_Y_st_ (_B_is_open_&_not_x_in_B_&_y_in_B_) take B = B; ::_thesis: ( B is open & not x in B & y in B ) thus B is open by A12; ::_thesis: ( not x in B & y in B ) thus not x in B by A14, XBOOLE_0:def_5; ::_thesis: y in B thus y in B by A14; ::_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; supposeA15: ( x in B & y in A \ B ) ; ::_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 ) ) now__::_thesis:_ex_B_being_Subset_of_Y_st_ (_B_is_open_&_x_in_B_&_not_y_in_B_) take B = B; ::_thesis: ( B is open & x in B & not y in B ) thus B is open by A12; ::_thesis: ( x in B & not y in B ) thus x in B by A15; ::_thesis: not y in B thus not y in B by A15, 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; suppose ( x in B & y in B ) ; ::_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 ) ) 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 ) ) by A3, A6, Def8; ::_thesis: verum end; end; 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; 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; hence A \/ B is T_0 by Def8; ::_thesis: verum end; theorem Th8: :: TSP_1:8 for Y being non empty TopStruct for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds A \/ B is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds A \/ B is T_0 let A, B be Subset of Y; ::_thesis: ( ( A is closed or B is closed ) & A is T_0 & B is T_0 implies A \/ B is T_0 ) assume A1: ( A is closed or B is closed ) ; ::_thesis: ( not A is T_0 or not B is T_0 or A \/ B is T_0 ) assume that A2: A is T_0 and A3: B is T_0 ; ::_thesis: A \/ B is T_0 now__::_thesis:_for_x,_y_being_Point_of_Y_st_x_in_A_\/_B_&_y_in_A_\/_B_&_x_<>_y_&_(_for_V_being_Subset_of_Y_holds_ (_not_V_is_closed_or_not_x_in_V_or_y_in_V_)_)_holds_ ex_W_being_Subset_of_Y_st_ (_W_is_closed_&_not_x_in_W_&_y_in_W_) let x, y be Point of Y; ::_thesis: ( x in A \/ B & y in A \/ B & x <> y & ( for V being Subset of Y holds ( not V is closed or not x in V or y in V ) ) implies ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) assume A4: ( x in A \/ B & y in A \/ B ) ; ::_thesis: ( not x <> y or ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39; assume A6: x <> y ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39; now__::_thesis:_(_ex_V_being_Subset_of_Y_st_ (_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_ (_W_is_closed_&_not_x_in_W_&_y_in_W_)_) percases ( A is closed or B is closed ) by A1; supposeA8: A is closed ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_(_ex_V_being_Subset_of_Y_st_ (_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_ (_W_is_closed_&_not_x_in_W_&_y_in_W_)_) percases ( ( x in A & y in A ) or ( x in A & y in B \ A ) or ( x in B \ A & y in A ) or ( x in B \ A & y in B \ A ) ) by A7, XBOOLE_0:def_3; suppose ( x in A & y in A ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) by A2, A6, Def9; ::_thesis: verum end; supposeA9: ( x in A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_ex_A_being_Subset_of_Y_st_ (_A_is_closed_&_x_in_A_&_not_y_in_A_) take A = A; ::_thesis: ( A is closed & x in A & not y in A ) thus A is closed by A8; ::_thesis: ( x in A & not y in A ) thus x in A by A9; ::_thesis: not y in A thus not y in A by A9, XBOOLE_0:def_5; ::_thesis: verum end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; supposeA10: ( x in B \ A & y in A ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_ex_A_being_Subset_of_Y_st_ (_A_is_closed_&_not_x_in_A_&_y_in_A_) take A = A; ::_thesis: ( A is closed & not x in A & y in A ) thus A is closed by A8; ::_thesis: ( not x in A & y in A ) thus not x in A by A10, XBOOLE_0:def_5; ::_thesis: y in A thus y in A by A10; ::_thesis: verum end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; supposeA11: ( x in B \ A & y in B \ A ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) B \ A c= B by XBOOLE_1:36; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) by A3, A6, A11, Def9; ::_thesis: verum end; end; end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; supposeA12: B is closed ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_(_ex_V_being_Subset_of_Y_st_ (_V_is_closed_&_x_in_V_&_not_y_in_V_)_or_ex_W_being_Subset_of_Y_st_ (_W_is_closed_&_not_x_in_W_&_y_in_W_)_) percases ( ( x in A \ B & y in A \ B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) or ( x in B & y in B ) ) by A5, XBOOLE_0:def_3; supposeA13: ( x in A \ B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) A \ B c= A by XBOOLE_1:36; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) by A2, A6, A13, Def9; ::_thesis: verum end; supposeA14: ( x in A \ B & y in B ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_ex_B_being_Subset_of_Y_st_ (_B_is_closed_&_not_x_in_B_&_y_in_B_) take B = B; ::_thesis: ( B is closed & not x in B & y in B ) thus B is closed by A12; ::_thesis: ( not x in B & y in B ) thus not x in B by A14, XBOOLE_0:def_5; ::_thesis: y in B thus y in B by A14; ::_thesis: verum end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; supposeA15: ( x in B & y in A \ B ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) now__::_thesis:_ex_B_being_Subset_of_Y_st_ (_B_is_closed_&_x_in_B_&_not_y_in_B_) take B = B; ::_thesis: ( B is closed & x in B & not y in B ) thus B is closed by A12; ::_thesis: ( x in B & not y in B ) thus x in B by A15; ::_thesis: not y in B thus not y in B by A15, XBOOLE_0:def_5; ::_thesis: verum end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; suppose ( x in B & y in B ) ; ::_thesis: ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) by A3, A6, Def9; ::_thesis: verum end; end; end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; end; end; hence ( ex V being Subset of Y st ( V is closed & x in V & not y in V ) or ex W being Subset of Y st ( W is closed & not x in W & y in W ) ) ; ::_thesis: verum end; hence A \/ B is T_0 by Def9; ::_thesis: verum end; theorem Th9: :: TSP_1:9 for Y being non empty TopStruct for A being Subset of Y st A is discrete holds A is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds A is T_0 let A be Subset of Y; ::_thesis: ( A is discrete implies A is T_0 ) assume A1: A is discrete ; ::_thesis: A is T_0 now__::_thesis:_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_) 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 that A2: x in A and A3: y in A ; ::_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 ) ) {x} c= A by A2, ZFMISC_1:31; then consider G being Subset of Y such that A4: G is open and A5: A /\ G = {x} by A1, TEX_2:def_3; assume A6: 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 ) ) now__::_thesis:_ex_G_being_Subset_of_Y_st_ (_G_is_open_&_x_in_G_&_not_y_in_G_) take G = G; ::_thesis: ( G is open & x in G & not y in G ) thus G is open by A4; ::_thesis: ( x in G & not y in G ) x in {x} by TARSKI:def_1; hence x in G by A5, XBOOLE_0:def_4; ::_thesis: not y in G now__::_thesis:_not_y_in_G assume y in G ; ::_thesis: contradiction then y in {x} by A3, A5, XBOOLE_0:def_4; hence contradiction by A6, TARSKI:def_1; ::_thesis: verum end; hence not y in G ; ::_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; hence A is T_0 by Def8; ::_thesis: verum end; theorem :: TSP_1:10 for Y being non empty TopStruct for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds not A is T_0 proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds not A is T_0 let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & not A is trivial implies not A is T_0 ) assume A1: A is anti-discrete ; ::_thesis: ( A is trivial or not A is T_0 ) consider s being set such that A2: s in A by XBOOLE_0:def_1; reconsider s0 = s as Element of A by A2; assume not A is trivial ; ::_thesis: not A is T_0 then A <> {s0} ; then consider t being set such that A3: t in A and A4: t <> s0 by ZFMISC_1:35; reconsider s = s, t = t as Point of Y by A2, A3; assume A5: A is T_0 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( ex E being Subset of Y st ( E is closed & s in E & not t in E ) or ex F being Subset of Y st ( F is closed & not s in F & t in F ) ) by A3, A4, A5, Def9; suppose ex E being Subset of Y st ( E is closed & s in E & not t in E ) ; ::_thesis: contradiction then consider E being Subset of Y such that A6: ( E is closed & s in E ) and A7: not t in E ; A c= E by A1, A2, A6, TEX_4:def_2; hence contradiction by A3, A7; ::_thesis: verum end; suppose ex F being Subset of Y st ( F is closed & not s in F & t in F ) ; ::_thesis: contradiction then consider F being Subset of Y such that A8: F is closed and A9: not s in F and A10: t in F ; A c= F by A1, A3, A8, A10, TEX_4:def_2; hence contradiction by A2, A9; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def10: :: TSP_1:def 10 for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y}; compatibility ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} ) proof thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y implies Cl {x} <> Cl {y} ) assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: Cl {x} <> Cl {y} now__::_thesis:_not_Cl_{x}_=_Cl_{y} percases ( ex V being Subset of X st ( V is open & x in V & not y in V ) or ex W being Subset of X st ( W is open & not x in W & y in W ) ) by A1, A2, Def8; suppose ex V being Subset of X st ( V is open & x in V & not y in V ) ; ::_thesis: not Cl {x} = Cl {y} then consider V being Subset of X such that A3: V is open and A4: x in V and A5: not y in V ; y in V ` by A5, SUBSET_1:29; then {y} c= V ` by ZFMISC_1:31; then A6: {y} misses V by SUBSET_1:23; assume A7: Cl {x} = Cl {y} ; ::_thesis: contradiction ( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def_1; then Cl {x} meets V by A4, XBOOLE_0:3; hence contradiction by A3, A6, A7, TSEP_1:36; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & not x in W & y in W ) ; ::_thesis: not Cl {x} = Cl {y} then consider W being Subset of X such that A8: W is open and A9: not x in W and A10: y in W ; x in W ` by A9, SUBSET_1:29; then {x} c= W ` by ZFMISC_1:31; then A11: {x} misses W by SUBSET_1:23; assume A12: Cl {x} = Cl {y} ; ::_thesis: contradiction ( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def_1; then Cl {y} meets W by A10, XBOOLE_0:3; hence contradiction by A8, A11, A12, TSEP_1:36; ::_thesis: verum end; end; end; hence Cl {x} <> Cl {y} ; ::_thesis: verum end; end; assume A13: for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} ; ::_thesis: A is T_0 now__::_thesis:_for_x,_y_being_Point_of_X_st_x_in_A_&_y_in_A_&_x_<>_y_&_(_for_E_being_Subset_of_X_st_E_is_closed_&_x_in_E_holds_ y_in_E_)_holds_ ex_F_being_Subset_of_X_st_ (_F_is_closed_&_not_x_in_F_&_y_in_F_) let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & ( for E being Subset of X st E is closed & x in E holds y in E ) implies ex F being Subset of X st ( F is closed & not x in F & y in F ) ) assume A14: ( x in A & y in A & x <> y ) ; ::_thesis: ( ( for E being Subset of X st E is closed & x in E holds y in E ) implies ex F being Subset of X st ( F is closed & not x in F & y in F ) ) assume A15: for E being Subset of X st E is closed & x in E holds y in E ; ::_thesis: ex F being Subset of X st ( F is closed & not x in F & y in F ) thus ex F being Subset of X st ( F is closed & not x in F & y in F ) ::_thesis: verum proof set F = Cl {y}; take Cl {y} ; ::_thesis: ( Cl {y} is closed & not x in Cl {y} & y in Cl {y} ) thus Cl {y} is closed ; ::_thesis: ( not x in Cl {y} & y in Cl {y} ) now__::_thesis:_not_x_in_Cl_{y} assume x in Cl {y} ; ::_thesis: contradiction then {x} c= Cl {y} by ZFMISC_1:31; then A16: Cl {x} c= Cl {y} by TOPS_1:5; y in Cl {x} by A15, Lm2; then {y} c= Cl {x} by ZFMISC_1:31; then Cl {y} c= Cl {x} by TOPS_1:5; then Cl {x} = Cl {y} by A16, XBOOLE_0:def_10; hence contradiction by A13, A14; ::_thesis: verum end; hence not x in Cl {y} ; ::_thesis: y in Cl {y} thus y in Cl {y} by Lm2; ::_thesis: verum end; end; hence A is T_0 by Def9; ::_thesis: verum end; end; :: deftheorem Def10 defines T_0 TSP_1:def_10_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def11: :: TSP_1:def 11 for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x}; compatibility ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} ) proof thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not y in Cl {x} ) assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: ( x in Cl {y} implies not y in Cl {x} ) assume that A3: x in Cl {y} and A4: y in Cl {x} ; ::_thesis: contradiction {y} c= Cl {x} by A4, ZFMISC_1:31; then A5: Cl {y} c= Cl {x} by TOPS_1:5; {x} c= Cl {y} by A3, ZFMISC_1:31; then Cl {x} c= Cl {y} by TOPS_1:5; then Cl {x} = Cl {y} by A5, XBOOLE_0:def_10; hence contradiction by A1, A2, Def10; ::_thesis: verum end; end; assume A6: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} ; ::_thesis: A is T_0 for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y} proof let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y implies Cl {x} <> Cl {y} ) assume A7: ( x in A & y in A & x <> y ) ; ::_thesis: Cl {x} <> Cl {y} assume A8: Cl {x} = Cl {y} ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( not x in Cl {y} or not y in Cl {x} ) by A6, A7; suppose not x in Cl {y} ; ::_thesis: contradiction hence contradiction by A8, Lm2; ::_thesis: verum end; suppose not y in Cl {x} ; ::_thesis: contradiction hence contradiction by A8, Lm2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence A is T_0 by Def10; ::_thesis: verum end; end; :: deftheorem Def11 defines T_0 TSP_1:def_11_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :: TSP_1:def 12 for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x}; compatibility ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) proof thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} hereby ::_thesis: verum let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not Cl {y} c= Cl {x} ) assume A2: ( x in A & y in A & x <> y ) ; ::_thesis: ( x in Cl {y} implies not Cl {y} c= Cl {x} ) assume x in Cl {y} ; ::_thesis: not Cl {y} c= Cl {x} then {x} c= Cl {y} by ZFMISC_1:31; then A3: Cl {x} c= Cl {y} by TOPS_1:5; assume Cl {y} c= Cl {x} ; ::_thesis: contradiction then Cl {x} = Cl {y} by A3, XBOOLE_0:def_10; hence contradiction by A1, A2, Def10; ::_thesis: verum end; end; assume A4: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ; ::_thesis: A is T_0 for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not y in Cl {x} proof let x, y be Point of X; ::_thesis: ( x in A & y in A & x <> y & x in Cl {y} implies not y in Cl {x} ) assume A5: ( x in A & y in A & x <> y ) ; ::_thesis: ( not x in Cl {y} or not y in Cl {x} ) assume A6: x in Cl {y} ; ::_thesis: not y in Cl {x} assume y in Cl {x} ; ::_thesis: contradiction then {y} c= Cl {x} by ZFMISC_1:31; hence contradiction by A4, A5, A6, TOPS_1:5; ::_thesis: verum end; hence A is T_0 by Def11; ::_thesis: verum end; end; :: deftheorem defines T_0 TSP_1:def_12_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds not Cl {y} c= Cl {x} ); theorem Th11: :: TSP_1:11 for X being non empty TopSpace for A being empty Subset of X holds A is T_0 proof let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds A is T_0 let A be empty Subset of X; ::_thesis: A is T_0 A is discrete by TEX_2:29; hence A is T_0 by Th9; ::_thesis: verum end; theorem :: TSP_1:12 for X being non empty TopSpace for x being Point of X holds {x} is T_0 by Th9, TEX_2:30; begin registration let Y be non empty TopStruct ; cluster non empty strict T_0 for SubSpace of Y; existence ex b1 being SubSpace of Y st ( b1 is strict & b1 is T_0 & not b1 is empty ) proof set X0 = the non empty trivial strict SubSpace of Y; take the non empty trivial strict SubSpace of Y ; ::_thesis: ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty ) thus ( the non empty trivial strict SubSpace of Y is strict & the non empty trivial strict SubSpace of Y is T_0 & not the non empty trivial strict SubSpace of Y is empty ) ; ::_thesis: verum end; end; Lm3: now__::_thesis:_for_Z_being_TopStruct_ for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z let Z be TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z [#] Z0 c= [#] Z by PRE_TOPC:def_4; hence the carrier of Z0 is Subset of Z ; ::_thesis: verum end; definition let Y be TopStruct ; let Y0 be SubSpace of Y; :: original: T_0 redefine attrY0 is T_0 means :: TSP_1:def 13 ( 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 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 ) ); compatibility ( Y0 is T_0 iff ( 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 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 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 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 ) ) ::_thesis: ( ( 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 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 ) ) implies Y0 is T_0 ) proof assume A1: Y0 is T_0 ; ::_thesis: ( 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 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 ) ) hereby ::_thesis: verum assume A2: not Y0 is empty ; ::_thesis: 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 open or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is open & not x in F & y in F ) let x, y be Point of Y; ::_thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds ( not E is open or not x in E or y in E ) ) implies ex F being Subset of Y st ( F is open & not x in F & y in F ) ) assume ( x is Point of Y0 & y is Point of Y0 ) ; ::_thesis: ( not x <> y or ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) then reconsider x0 = x, y0 = y as Point of Y0 ; assume A3: x <> y ; ::_thesis: ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) now__::_thesis:_(_ex_E_being_Subset_of_Y_st_ (_E_is_open_&_x_in_E_&_not_y_in_E_)_or_ex_F_being_Subset_of_Y_st_ (_F_is_open_&_not_x_in_F_&_y_in_F_)_) percases ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) by A1, A2, A3, Def3; suppose ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) ; ::_thesis: ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) then consider E0 being Subset of Y0 such that A4: E0 is open and A5: x0 in E0 and A6: not y0 in E0 ; now__::_thesis:_ex_E_being_Subset_of_Y_st_ (_E_is_open_&_x_in_E_&_not_y_in_E_) consider E being Subset of Y such that A7: E is open and A8: E0 = E /\ A by A4, Def1; take E = E; ::_thesis: ( E is open & x in E & not y in E ) thus E is open by A7; ::_thesis: ( x in E & not y in E ) E /\ A c= E by XBOOLE_1:17; hence x in E by A5, A8; ::_thesis: not y in E thus not y in E by A2, A6, A8, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) ; ::_thesis: verum end; suppose ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ; ::_thesis: ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) then consider F0 being Subset of Y0 such that A9: F0 is open and A10: not x0 in F0 and A11: y0 in F0 ; now__::_thesis:_ex_F_being_Subset_of_Y_st_ (_F_is_open_&_not_x_in_F_&_y_in_F_) consider F being Subset of Y such that A12: F is open and A13: F0 = F /\ A by A9, Def1; take F = F; ::_thesis: ( F is open & not x in F & y in F ) thus F is open by A12; ::_thesis: ( not x in F & y in F ) thus not x in F by A2, A10, A13, XBOOLE_0:def_4; ::_thesis: y in F F /\ A c= F by XBOOLE_1:17; hence y in F by A11, A13; ::_thesis: verum end; hence ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) ; ::_thesis: verum end; end; end; hence ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) ; ::_thesis: verum end; end; assume A14: ( 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 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 ) ) ; ::_thesis: Y0 is T_0 now__::_thesis:_(_not_Y0_is_empty_implies_for_x0,_y0_being_Point_of_Y0_holds_ (_not_x0_<>_y0_or_ex_E0_being_Subset_of_Y0_st_ (_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_ (_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_)_)_) A15: the carrier of Y0 c= the carrier of Y by Def1; assume A16: not Y0 is empty ; ::_thesis: for x0, y0 being Point of Y0 holds ( not x0 <> y0 or ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) let x0, y0 be Point of Y0; ::_thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) the carrier of Y0 <> {} by A16; then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ; then reconsider x = x0, y = y0 as Point of Y by A15; assume A17: x0 <> y0 ; ::_thesis: ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) now__::_thesis:_(_ex_E0_being_Subset_of_Y0_st_ (_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_)_or_ex_F0_being_Subset_of_Y0_st_ (_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_)_) percases ( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st ( F is open & not x in F & y in F ) ) by A14, A16, A17; suppose ex E being Subset of Y st ( E is open & x in E & not y in E ) ; ::_thesis: ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) then consider E being Subset of Y such that A18: E is open and A19: x in E and A20: not y in E ; now__::_thesis:_ex_E0_being_Subset_of_Y0_st_ (_E0_is_open_&_x0_in_E0_&_not_y0_in_E0_) consider E0 being Subset of Y0 such that A21: E0 is open and A22: E0 = E /\ A by A18, Th1; take E0 = E0; ::_thesis: ( E0 is open & x0 in E0 & not y0 in E0 ) thus E0 is open by A21; ::_thesis: ( x0 in E0 & not y0 in E0 ) thus x0 in E0 by A16, A19, A22, XBOOLE_0:def_4; ::_thesis: not y0 in E0 now__::_thesis:_not_y0_in_E0 A23: E /\ A c= E by XBOOLE_1:17; assume y0 in E0 ; ::_thesis: contradiction hence contradiction by A20, A22, A23; ::_thesis: verum end; hence not y0 in E0 ; ::_thesis: verum end; hence ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum end; suppose ex F being Subset of Y st ( F is open & not x in F & y in F ) ; ::_thesis: ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) then consider F being Subset of Y such that A24: F is open and A25: not x in F and A26: y in F ; now__::_thesis:_ex_F0_being_Subset_of_Y0_st_ (_F0_is_open_&_not_x0_in_F0_&_y0_in_F0_) consider F0 being Subset of Y0 such that A27: F0 is open and A28: F0 = F /\ A by A24, Th1; take F0 = F0; ::_thesis: ( F0 is open & not x0 in F0 & y0 in F0 ) thus F0 is open by A27; ::_thesis: ( not x0 in F0 & y0 in F0 ) now__::_thesis:_not_x0_in_F0 A29: F /\ A c= F by XBOOLE_1:17; assume x0 in F0 ; ::_thesis: contradiction hence contradiction by A25, A28, A29; ::_thesis: verum end; hence not x0 in F0 ; ::_thesis: y0 in F0 thus y0 in F0 by A16, A26, A28, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum end; end; end; hence ( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 ) ) ; ::_thesis: verum end; hence Y0 is T_0 by Def3; ::_thesis: verum end; end; :: deftheorem defines T_0 TSP_1:def_13_:_ for Y being TopStruct for Y0 being SubSpace of Y holds ( Y0 is T_0 iff ( 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 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 ) ) ); definition let Y be TopStruct ; let Y0 be SubSpace of Y; :: original: T_0 redefine attrY0 is T_0 means :Def14: :: TSP_1:def 14 ( 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 ) ); compatibility ( Y0 is T_0 iff ( 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 ) ) ) proof reconsider A = the carrier of Y0 as Subset of Y by Lm3; thus ( not Y0 is V138() 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: ( ( 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 ) ) implies Y0 is T_0 ) proof assume A1: Y0 is V138() ; ::_thesis: ( 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 ) ) hereby ::_thesis: verum assume A2: not Y0 is empty ; ::_thesis: 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 ) let x, y be Point of Y; ::_thesis: ( 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 ) ) implies ex F being Subset of Y st ( F is closed & not x in F & y in F ) ) assume ( x is Point of Y0 & y is Point of Y0 ) ; ::_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 ) ) then reconsider x0 = x, y0 = y as Point of Y0 ; 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 ) ) now__::_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_)_) percases ( 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 ) ) by A1, A2, A3, Def4; suppose ex E0 being Subset of Y0 st ( E0 is closed & x0 in E0 & not y0 in E0 ) ; ::_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 E0 being Subset of Y0 such that A4: E0 is closed and A5: x0 in E0 and A6: not y0 in E0 ; now__::_thesis:_ex_E_being_Subset_of_Y_st_ (_E_is_closed_&_x_in_E_&_not_y_in_E_) consider E being Subset of Y such that A7: E is closed and A8: E0 = E /\ A by A4, Def2; take E = E; ::_thesis: ( E is closed & x in E & not y in E ) thus E is closed by A7; ::_thesis: ( x in E & not y in E ) E /\ A c= E by XBOOLE_1:17; hence x in E by A5, A8; ::_thesis: not y in E thus not y in E by A2, A6, A8, XBOOLE_0:def_4; ::_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 F0 being Subset of Y0 st ( F0 is closed & not x0 in F0 & y0 in F0 ) ; ::_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 F0 being Subset of Y0 such that A9: F0 is closed and A10: not x0 in F0 and A11: y0 in F0 ; now__::_thesis:_ex_F_being_Subset_of_Y_st_ (_F_is_closed_&_not_x_in_F_&_y_in_F_) consider F being Subset of Y such that A12: F is closed and A13: F0 = F /\ A by A9, Def2; take F = F; ::_thesis: ( F is closed & not x in F & y in F ) thus F is closed by A12; ::_thesis: ( not x in F & y in F ) thus not x in F by A2, A10, A13, XBOOLE_0:def_4; ::_thesis: y in F F /\ A c= F by XBOOLE_1:17; hence y in F by A11, A13; ::_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; 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; assume A14: ( 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: Y0 is T_0 now__::_thesis:_(_not_Y0_is_empty_implies_for_x0,_y0_being_Point_of_Y0_holds_ (_not_x0_<>_y0_or_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_)_)_) A15: the carrier of Y0 c= the carrier of Y by Def1; assume A16: not Y0 is empty ; ::_thesis: for x0, y0 being Point of Y0 holds ( not x0 <> y0 or 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 ) ) let x0, y0 be Point of Y0; ::_thesis: ( not x0 <> y0 or 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 ) ) the carrier of Y0 <> {} by A16; then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ; then reconsider x = x0, y = y0 as Point of Y by A15; assume A17: x0 <> y0 ; ::_thesis: ( 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 ) ) now__::_thesis:_(_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_)_) percases ( 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 A14, A16, A17; suppose ex E being Subset of Y st ( E is closed & x in E & not y in E ) ; ::_thesis: ( 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 ) ) then consider E being Subset of Y such that A18: E is closed and A19: x in E and A20: not y in E ; now__::_thesis:_ex_E0_being_Subset_of_Y0_st_ (_E0_is_closed_&_x0_in_E0_&_not_y0_in_E0_) consider E0 being Subset of Y0 such that A21: E0 is closed and A22: E0 = E /\ A by A18, Th2; take E0 = E0; ::_thesis: ( E0 is closed & x0 in E0 & not y0 in E0 ) thus E0 is closed by A21; ::_thesis: ( x0 in E0 & not y0 in E0 ) thus x0 in E0 by A16, A19, A22, XBOOLE_0:def_4; ::_thesis: not y0 in E0 now__::_thesis:_not_y0_in_E0 A23: E /\ A c= E by XBOOLE_1:17; assume y0 in E0 ; ::_thesis: contradiction hence contradiction by A20, A22, A23; ::_thesis: verum end; hence not y0 in E0 ; ::_thesis: verum 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: verum end; suppose ex F being Subset of Y st ( F is closed & not x in F & y in F ) ; ::_thesis: ( 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 ) ) then consider F being Subset of Y such that A24: F is closed and A25: not x in F and A26: y in F ; now__::_thesis:_ex_F0_being_Subset_of_Y0_st_ (_F0_is_closed_&_not_x0_in_F0_&_y0_in_F0_) consider F0 being Subset of Y0 such that A27: F0 is closed and A28: F0 = F /\ A by A24, Th2; take F0 = F0; ::_thesis: ( F0 is closed & not x0 in F0 & y0 in F0 ) thus F0 is closed by A27; ::_thesis: ( not x0 in F0 & y0 in F0 ) now__::_thesis:_not_x0_in_F0 A29: F /\ A c= F by XBOOLE_1:17; assume x0 in F0 ; ::_thesis: contradiction hence contradiction by A25, A28, A29; ::_thesis: verum end; hence not x0 in F0 ; ::_thesis: y0 in F0 thus y0 in F0 by A16, A26, A28, XBOOLE_0:def_4; ::_thesis: verum 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: verum end; end; 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: verum end; hence Y0 is T_0 by Def4; ::_thesis: verum end; end; :: deftheorem Def14 defines T_0 TSP_1:def_14_:_ for Y being TopStruct for Y0 being SubSpace of Y holds ( Y0 is T_0 iff ( 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 ) ) ); theorem Th13: :: TSP_1:13 for Y being non empty TopStruct for Y0 being non empty SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is T_0 iff Y0 is V138() ) proof let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is T_0 iff Y0 is V138() ) let Y0 be non empty SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds ( A is T_0 iff Y0 is V138() ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is T_0 iff Y0 is V138() ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( A is T_0 iff Y0 is V138() ) hereby ::_thesis: ( Y0 is V138() implies A is T_0 ) assume A is T_0 ; ::_thesis: Y0 is V138() then 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 ) by A1, Def9; hence Y0 is V138() by Def14; ::_thesis: verum end; hereby ::_thesis: verum assume Y0 is V138() ; ::_thesis: A is T_0 then 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 ) by A1, Def14; hence A is T_0 by Def9; ::_thesis: verum end; end; theorem :: TSP_1:14 for Y being non empty TopStruct for Y0 being non empty SubSpace of Y for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds Y0 is V138() proof let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds Y0 is V138() let Y0 be non empty SubSpace of Y; ::_thesis: for Y1 being non empty V138() SubSpace of Y st Y0 is SubSpace of Y1 holds Y0 is V138() let Y1 be non empty V138() SubSpace of Y; ::_thesis: ( Y0 is SubSpace of Y1 implies Y0 is V138() ) reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty Subset of Y by Lm3; assume A1: Y0 is SubSpace of Y1 ; ::_thesis: Y0 is V138() A2: A1 is T_0 by Th13; ( [#] Y0 = A0 & [#] Y1 = A1 ) ; then A0 c= A1 by A1, PRE_TOPC:def_4; then A0 is T_0 by A2, Th5; hence Y0 is V138() by Th13; ::_thesis: verum end; theorem :: TSP_1:15 for X being non empty TopSpace for X1 being non empty V138() SubSpace of X for X2 being non empty SubSpace of X st X1 meets X2 holds X1 meet X2 is V138() proof let X be non empty TopSpace; ::_thesis: for X1 being non empty V138() SubSpace of X for X2 being non empty SubSpace of X st X1 meets X2 holds X1 meet X2 is V138() let X1 be non empty V138() SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 meets X2 holds X1 meet X2 is V138() let X2 be non empty SubSpace of X; ::_thesis: ( X1 meets X2 implies X1 meet X2 is V138() ) reconsider A1 = the carrier of X1 as non empty Subset of X by TSEP_1:1; reconsider A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1; assume X1 meets X2 ; ::_thesis: X1 meet X2 is V138() then A1: the carrier of (X1 meet X2) = A1 /\ A2 by TSEP_1:def_4; A1 is T_0 by Th13; then A1 /\ A2 is T_0 by Th6; hence X1 meet X2 is V138() by A1, Th13; ::_thesis: verum end; theorem :: TSP_1:16 for X being non empty TopSpace for X1, X2 being non empty V138() SubSpace of X st ( X1 is open or X2 is open ) holds X1 union X2 is V138() proof let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty V138() SubSpace of X st ( X1 is open or X2 is open ) holds X1 union X2 is V138() let X1, X2 be non empty V138() SubSpace of X; ::_thesis: ( ( X1 is open or X2 is open ) implies X1 union X2 is V138() ) reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1; assume ( X1 is open or X2 is open ) ; ::_thesis: X1 union X2 is V138() then A1: ( A1 is open or A2 is open ) by TSEP_1:16; ( A1 is T_0 & A2 is T_0 ) by Th13; then ( the carrier of (X1 union X2) = A1 \/ A2 & A1 \/ A2 is T_0 ) by A1, Th7, TSEP_1:def_2; hence X1 union X2 is V138() by Th13; ::_thesis: verum end; theorem :: TSP_1:17 for X being non empty TopSpace for X1, X2 being non empty V138() SubSpace of X st ( X1 is closed or X2 is closed ) holds X1 union X2 is V138() proof let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty V138() SubSpace of X st ( X1 is closed or X2 is closed ) holds X1 union X2 is V138() let X1, X2 be non empty V138() SubSpace of X; ::_thesis: ( ( X1 is closed or X2 is closed ) implies X1 union X2 is V138() ) reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1; assume ( X1 is closed or X2 is closed ) ; ::_thesis: X1 union X2 is V138() then A1: ( A1 is closed or A2 is closed ) by TSEP_1:11; ( A1 is T_0 & A2 is T_0 ) by Th13; then ( the carrier of (X1 union X2) = A1 \/ A2 & A1 \/ A2 is T_0 ) by A1, Th8, TSEP_1:def_2; hence X1 union X2 is V138() by Th13; ::_thesis: verum end; definition let X be non empty TopSpace; mode Kolmogorov_subspace of X is non empty V138() SubSpace of X; end; theorem :: TSP_1:18 for X being non empty TopSpace for A0 being non empty Subset of X st A0 is T_0 holds ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 proof let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is T_0 holds ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 let A0 be non empty Subset of X; ::_thesis: ( A0 is T_0 implies ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 ) consider X0 being non empty strict SubSpace of X such that A1: A0 = the carrier of X0 by TSEP_1:10; assume A0 is T_0 ; ::_thesis: ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 then reconsider X0 = X0 as strict Kolmogorov_subspace of X by A1, Th13; take X0 ; ::_thesis: A0 = the carrier of X0 thus A0 = the carrier of X0 by A1; ::_thesis: verum end; registration let X be non trivial TopSpace; cluster non empty strict T_0 proper for SubSpace of X; existence ex b1 being Kolmogorov_subspace of X st ( b1 is proper & b1 is strict ) proof set X0 = the non empty trivial strict SubSpace of X; take the non empty trivial strict SubSpace of X ; ::_thesis: ( the non empty trivial strict SubSpace of X is proper & the non empty trivial strict SubSpace of X is strict ) thus ( the non empty trivial strict SubSpace of X is proper & the non empty trivial strict SubSpace of X is strict ) ; ::_thesis: verum end; end; registration let X be Kolmogorov_space; cluster non empty -> non empty V138() for SubSpace of X; coherence for b1 being non empty SubSpace of X holds b1 is V138() proof let X0 be non empty SubSpace of X; ::_thesis: X0 is V138() reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1; X is SubSpace of X by TSEP_1:2; then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1; A is T_0 by Th4; then A0 is T_0 by Th5; hence X0 is V138() by Th13; ::_thesis: verum end; end; registration let X be non-Kolmogorov_space; cluster non empty non proper -> non empty V138() for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is proper holds not b1 is V138() proof let X0 be non empty SubSpace of X; ::_thesis: ( not X0 is proper implies not X0 is V138() ) reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1; X is SubSpace of X by TSEP_1:2; then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1; assume not X0 is proper ; ::_thesis: X0 is V138() then not A0 is proper by TEX_2:8; then A0 = A by SUBSET_1:def_6; then not A0 is T_0 by Th4; hence X0 is V138() by Th13; ::_thesis: verum end; cluster non empty V138() -> non empty proper for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is V138() holds b1 is proper ; end; registration let X be non-Kolmogorov_space; cluster strict V138() for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is strict & b1 is V138() ) proof set X0 = the non empty strict non proper SubSpace of X; take the non empty strict non proper SubSpace of X ; ::_thesis: ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is V138() ) thus ( the non empty strict non proper SubSpace of X is strict & the non empty strict non proper SubSpace of X is V138() ) ; ::_thesis: verum end; end; definition let X be non-Kolmogorov_space; mode non-Kolmogorov_subspace of X is V138() SubSpace of X; end; theorem :: TSP_1:19 for X being non-Kolmogorov_space for A0 being Subset of X st not A0 is T_0 holds ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 proof let X be non-Kolmogorov_space; ::_thesis: for A0 being Subset of X st not A0 is T_0 holds ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 let A0 be Subset of X; ::_thesis: ( not A0 is T_0 implies ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 ) assume A1: not A0 is T_0 ; ::_thesis: ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 then not A0 is empty by Th11; then consider X0 being non empty strict SubSpace of X such that A2: A0 = the carrier of X0 by TSEP_1:10; reconsider X0 = X0 as strict V138() SubSpace of X by A1, A2, Th13; take X0 ; ::_thesis: A0 = the carrier of X0 thus A0 = the carrier of X0 by A2; ::_thesis: verum end;