tsp_1.miz



    begin

    definition

      let Y be TopStruct;

      :: original: SubSpace

      redefine

      :: TSP_1:def1

      mode SubSpace of Y means

      : Def1: the carrier of it c= the carrier of Y & for G0 be Subset of it holds G0 is open iff ex G be Subset of Y st G is open & G0 = (G /\ the carrier of it );

      compatibility

      proof

        let Y0 be TopStruct;

        

         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 be Subset of Y0 holds G0 is open iff ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0)

        proof

          assume

           A2: Y0 is SubSpace of Y;

          hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4;

          thus for G0 be Subset of Y0 holds G0 is open iff ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0)

          proof

            let G0 be Subset of Y0;

            thus G0 is open implies ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0)

            proof

              assume G0 is open;

              then G0 in the topology of Y0 by PRE_TOPC:def 2;

              then

              consider G be 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 as Subset of Y;

              take G;

              thus G is open by A3, PRE_TOPC:def 2;

              thus thesis by A4;

            end;

            given G be Subset of Y such that

             A5: G is open and

             A6: G0 = (G /\ the carrier of Y0);

            G in the topology of Y & G0 = (G /\ ( [#] Y0)) by A6, A5, PRE_TOPC:def 2;

            then G0 in the topology of Y0 by A2, PRE_TOPC:def 4;

            hence thesis by PRE_TOPC:def 2;

          end;

        end;

        assume that

         A7: the carrier of Y0 c= the carrier of Y and

         A8: for G0 be Subset of Y0 holds G0 is open iff ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0);

        

         A9: for G0 be Subset of Y0 holds G0 in the topology of Y0 iff ex G be Subset of Y st G in the topology of Y & G0 = (G /\ ( [#] Y0))

        proof

          let G0 be Subset of Y0;

          reconsider M = G0 as Subset of Y0;

          thus G0 in the topology of Y0 implies ex G be Subset of Y st G in the topology of Y & G0 = (G /\ ( [#] Y0))

          proof

            reconsider M = G0 as Subset of Y0;

            assume G0 in the topology of Y0;

            then M is open by PRE_TOPC:def 2;

            then

            consider G be Subset of Y such that

             A10: G is open and

             A11: G0 = (G /\ the carrier of Y0) by A8;

            take G;

            thus G in the topology of Y by A10, PRE_TOPC:def 2;

            thus thesis by A11;

          end;

          given G be Subset of Y such that

           A12: G in the topology of Y and

           A13: G0 = (G /\ ( [#] Y0));

          reconsider G as Subset of Y;

          G is open & G0 = (G /\ the carrier of Y0) by A13, A12, PRE_TOPC:def 2;

          then M is open by A8;

          hence thesis by PRE_TOPC:def 2;

        end;

        ( [#] Y0) c= ( [#] Y) by A7;

        hence thesis by A9, PRE_TOPC:def 4;

      end;

    end

    theorem :: TSP_1:1

    

     Th1: for Y be TopStruct, Y0 be SubSpace of Y holds for G be Subset of Y st G is open holds ex G0 be Subset of Y0 st G0 is open & G0 = (G /\ the carrier of Y0)

    proof

      let Y be TopStruct, Y0 be SubSpace of Y;

      let G be Subset of Y;

      assume

       A1: G is open;

      ( [#] 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;

      thus G0 is open by A1, Def1;

      thus thesis;

    end;

    definition

      let Y be TopStruct;

      :: original: SubSpace

      redefine

      :: TSP_1:def2

      mode SubSpace of Y means

      : Def2: the carrier of it c= the carrier of Y & for F0 be Subset of it holds F0 is closed iff ex F be Subset of Y st F is closed & F0 = (F /\ the carrier of it );

      compatibility

      proof

        let Y0 be TopStruct;

        

         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 be Subset of Y0 holds F0 is closed iff ex F be Subset of Y st F is closed & F0 = (F /\ the carrier of Y0)

        proof

          assume

           A2: Y0 is SubSpace of Y;

          hence the carrier of Y0 c= the carrier of Y by A1, PRE_TOPC:def 4;

          ( [#] Y0) c= ( [#] Y) by A2, PRE_TOPC:def 4;

          then

           A3: (( [#] Y0) \ ( [#] Y)) = {} by XBOOLE_1: 37;

          thus for F0 be Subset of Y0 holds F0 is closed iff ex F be Subset of Y st F is closed & F0 = (F /\ the carrier of Y0)

          proof

            let F0 be Subset of Y0;

            set G0 = (( [#] Y0) \ F0);

            thus F0 is closed implies ex F be Subset of Y st F is closed & F0 = (F /\ the carrier of Y0)

            proof

              assume F0 is closed;

              then (( [#] Y0) \ F0) is open by PRE_TOPC:def 3;

              then

              consider G be 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);

              

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

              hence F is closed by A4, PRE_TOPC:def 3;

              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 thesis;

            end;

            given F be Subset of Y such that

             A7: F is closed and

             A8: F0 = (F /\ the carrier of Y0);

            now

              take G = (( [#] Y) \ F);

              

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

              thus G is open by A7, PRE_TOPC:def 3;

              G0 = ((( [#] 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 G0 = (G /\ the carrier of Y0);

            end;

            then G0 is open by A2, Def1;

            hence thesis by PRE_TOPC:def 3;

          end;

        end;

        assume that

         A10: the carrier of Y0 c= the carrier of Y and

         A11: for F0 be Subset of Y0 holds F0 is closed iff ex F be Subset of Y st F is closed & F0 = (F /\ the carrier of Y0);

        

         A12: (( [#] Y0) \ ( [#] Y)) = {} by A10, XBOOLE_1: 37;

        for G0 be Subset of Y0 holds G0 is open iff ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0)

        proof

          let G0 be Subset of Y0;

          set F0 = (( [#] Y0) \ G0);

          thus G0 is open implies ex G be Subset of Y st G is open & G0 = (G /\ the carrier of Y0)

          proof

            set F0 = (( [#] Y0) \ G0);

            

             A13: G0 = (( [#] Y0) \ F0) by PRE_TOPC: 3;

            assume G0 is open;

            then F0 is closed by A13, PRE_TOPC:def 3;

            then

            consider F be Subset of Y such that

             A14: F is closed and

             A15: F0 = (F /\ the carrier of Y0) by A11;

            take G = (( [#] Y) \ F);

            thus G is open by A14, PRE_TOPC:def 3;

            

             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 thesis;

          end;

          given G be Subset of Y such that

           A17: G is open and

           A18: G0 = (G /\ the carrier of Y0);

          now

            take F = (( [#] Y) \ G);

            

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

            hence F is closed by A17, PRE_TOPC:def 3;

            F0 = ((( [#] 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 F0 = (F /\ the carrier of Y0);

          end;

          then G0 = (( [#] Y0) \ F0) & F0 is closed by A11, PRE_TOPC: 3;

          hence thesis by PRE_TOPC:def 3;

        end;

        hence Y0 is SubSpace of Y by A10, Def1;

      end;

    end

    theorem :: TSP_1:2

    

     Th2: for Y be TopStruct, Y0 be SubSpace of Y holds for F be Subset of Y st F is closed holds ex F0 be Subset of Y0 st F0 is closed & F0 = (F /\ the carrier of Y0)

    proof

      let Y be TopStruct, Y0 be SubSpace of Y;

      let F be Subset of Y;

      assume

       A1: F is closed;

      ( [#] 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;

      thus F0 is closed by A1, Def2;

      thus thesis;

    end;

    begin

    definition

      let T be TopStruct;

      :: original: T_0

      redefine

      :: TSP_1:def3

      attr T is T_0 means T is empty or for x,y be Point of T st x <> y holds (ex V be Subset of T st V is open & x in V & not y in V) or ex W be Subset of T st W is open & not x in W & y in W;

      compatibility

      proof

        hereby

          assume

           A1: T is T_0;

          assume

           A2: not T is empty;

          let x,y be Point of T;

          assume x <> y;

          then ex V be 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;

          hence (ex V be Subset of T st V is open & x in V & not y in V) or ex W be Subset of T st W is open & not x in W & y in W;

        end;

        assume

         A3: T is empty or for x,y be Point of T st x <> y holds (ex V be Subset of T st V is open & x in V & not y in V) or ex W be Subset of T st W is open & not x in W & y in W;

        assume

         A4: not T is empty;

        let x,y be Point of T;

        assume x <> y;

        then (ex V be Subset of T st V is open & x in V & not y in V) or ex W be Subset of T st W is open & not x in W & y in W by A3, A4;

        hence thesis;

      end;

    end

    definition

      let Y be TopStruct;

      :: original: T_0

      redefine

      :: TSP_1:def4

      attr Y is T_0 means Y is empty or for x,y be Point of Y st x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

      compatibility

      proof

        thus Y is T_0 implies Y is empty or for x,y be Point of Y st x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F

        proof

          assume

           A1: Y is empty or for x,y be Point of Y st x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W;

          assume

           A2: not Y is empty;

          let x,y be Point of Y;

          assume

           A3: x <> y;

          hereby

            per cases by A1, A2, A3;

              suppose ex V be Subset of Y st V is open & x in V & not y in V;

              then

              consider V be Subset of Y such that

               A4: V is open and

               A5: x in V and

               A6: not y in V;

              now

                take F = (V ` );

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

                hence F is closed by A4, PRE_TOPC:def 3;

                thus not x in F by A5, XBOOLE_0:def 5;

                thus y in F by A2, A6, SUBSET_1: 29;

              end;

              hence thesis;

            end;

              suppose ex W be Subset of Y st W is open & not x in W & y in W;

              then

              consider W be Subset of Y such that

               A7: W is open and

               A8: not x in W and

               A9: y in W;

              now

                take E = (W ` );

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

                hence E is closed by A7, PRE_TOPC:def 3;

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

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

              end;

              hence thesis;

            end;

          end;

        end;

        assume

         A10: Y is empty or for x,y be Point of Y st x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

         not Y is empty implies for x,y be Point of Y st x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W

        proof

          assume

           A11: not Y is empty;

          let x,y be Point of Y;

          assume

           A12: x <> y;

          hereby

            per cases by A10, A11, A12;

              suppose ex E be Subset of Y st E is closed & x in E & not y in E;

              then

              consider E be Subset of Y such that

               A13: E is closed and

               A14: x in E and

               A15: not y in E;

              now

                take W = (E ` );

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

                hence W is open by A13, PRE_TOPC:def 3;

                thus not x in W by A14, XBOOLE_0:def 5;

                thus y in W by A11, A15, SUBSET_1: 29;

              end;

              hence thesis;

            end;

              suppose ex F be Subset of Y st F is closed & not x in F & y in F;

              then

              consider F be Subset of Y such that

               A16: F is closed and

               A17: not x in F and

               A18: y in F;

              now

                take V = (F ` );

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

                hence V is open by A16, PRE_TOPC:def 3;

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

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

              end;

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      cluster trivial -> T_0 for non empty TopStruct;

      coherence

      proof

        let Y be non empty TopStruct;

        assume Y is trivial;

        then

        consider a be Point of Y such that

         A1: the carrier of Y = {a} by TEX_1:def 1;

        now

          let x,y be Point of Y;

          assume

           A2: x <> y;

          x = a by A1, TARSKI:def 1;

          hence (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W by A1, A2, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    

     Lm1: for X be anti-discrete non trivial TopStruct holds X is non T_0

    proof

      let X be anti-discrete non trivial TopStruct;

      now

        consider x,y be Point of X such that

         A1: x <> y by STRUCT_0:def 10;

        take x, y;

        thus x <> y by A1;

         A2:

        now

          let V be Subset of X;

          assume V is open;

          then

           A3: V = {} or V = the carrier of X by TDLAT_3: 18;

          assume y in V;

          hence x in V by A3;

        end;

        now

          let V be Subset of X;

          assume V is open;

          then

           A4: V = {} or V = the carrier of X by TDLAT_3: 18;

          assume x in V;

          hence y in V by A4;

        end;

        hence not (ex V be Subset of X st V is open & x in V & not y in V) & not (ex W be Subset of X st W is open & not x in W & y in W) by A2;

      end;

      hence thesis;

    end;

    registration

      cluster strict T_0 non empty for TopSpace;

      existence

      proof

        set X = the trivial strict non empty TopSpace;

        take X;

        thus thesis;

      end;

      cluster strict non T_0 non empty for TopSpace;

      existence

      proof

        set X = the anti-discrete non trivial strict non empty TopSpace;

        take X;

        thus thesis by Lm1;

      end;

    end

    registration

      cluster discrete -> T_0 for non empty TopSpace;

      coherence

      proof

        let Y be non empty TopSpace;

        assume

         A1: Y is discrete;

        now

          let x,y be Point of Y;

          assume

           A2: x <> y;

          now

            take V = {x};

            thus V is open by A1, TDLAT_3: 15;

            thus x in V by TARSKI:def 1;

            thus not y in V by A2, TARSKI:def 1;

          end;

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

        end;

        hence thesis;

      end;

      cluster non T_0 -> non discrete for non empty TopSpace;

      coherence ;

      cluster anti-discrete non trivial -> non T_0 for non empty TopSpace;

      coherence by Lm1;

      cluster anti-discrete T_0 -> trivial for non empty TopSpace;

      coherence ;

      cluster T_0 non trivial -> non anti-discrete for non empty TopSpace;

      coherence ;

    end

    

     Lm2: for X be non empty TopSpace, x be Point of X holds x in ( Cl {x})

    proof

      let X be non empty TopSpace, x be Point of X;

      x in {x} & {x} c= ( Cl {x}) by PRE_TOPC: 18, TARSKI:def 1;

      hence thesis;

    end;

    definition

      let X be non empty TopSpace;

      :: original: T_0

      redefine

      :: TSP_1:def5

      attr X is T_0 means for x,y be Point of X st x <> y holds ( Cl {x}) <> ( Cl {y});

      compatibility

      proof

        thus X is T_0 implies for x,y be Point of X st x <> y holds ( Cl {x}) <> ( Cl {y})

        proof

          assume

           A1: X is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x <> y;

            now

              per cases by A1, A2;

                suppose ex V be Subset of X st V is open & x in V & not y in V;

                then

                consider V be 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});

                hence contradiction by A7, A6, XBOOLE_0:def 7;

              end;

                suppose ex W be Subset of X st W is open & not x in W & y in W;

                then

                consider W be 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});

                hence contradiction by A12, A11, XBOOLE_0:def 7;

              end;

            end;

            hence ( Cl {x}) <> ( Cl {y});

          end;

        end;

        assume

         A13: for x,y be Point of X st x <> y holds ( Cl {x}) <> ( Cl {y});

        now

          let x,y be Point of X;

          assume

           A14: x <> y;

          assume

           A15: for E be Subset of X st E is closed & x in E holds y in E;

          thus ex F be Subset of X st F is closed & not x in F & y in F

          proof

            set F = ( Cl {y});

            take F;

            thus F is closed;

            now

              assume x in F;

              then {x} c= F by ZFMISC_1: 31;

              then

               A16: ( Cl {x}) c= F by TOPS_1: 5;

              y in ( Cl {x}) by A15, Lm2;

              then {y} c= ( Cl {x}) by ZFMISC_1: 31;

              then F c= ( Cl {x}) by TOPS_1: 5;

              then ( Cl {x}) = F by A16, XBOOLE_0:def 10;

              hence contradiction by A13, A14;

            end;

            hence not x in F;

            thus thesis by Lm2;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      :: original: T_0

      redefine

      :: TSP_1:def6

      attr X is T_0 means for x,y be Point of X st x <> y holds not x in ( Cl {y}) or not y in ( Cl {x});

      compatibility

      proof

        thus X is T_0 implies for x,y be Point of X st x <> y holds not x in ( Cl {y}) or not y in ( Cl {x})

        proof

          assume

           A1: X is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x <> y;

            assume that

             A3: x in ( Cl {y}) and

             A4: y in ( Cl {x});

             {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;

          end;

        end;

        assume

         A6: for x,y be Point of X st x <> y holds not x in ( Cl {y}) or not y in ( Cl {x});

        for x,y be Point of X st x <> y holds ( Cl {x}) <> ( Cl {y})

        proof

          let x,y be Point of X;

          assume

           A7: x <> y;

          assume

           A8: ( Cl {x}) = ( Cl {y});

          now

            per cases by A6, A7;

              suppose not x in ( Cl {y});

              hence contradiction by A8, Lm2;

            end;

              suppose not y in ( Cl {x});

              hence contradiction by A8, Lm2;

            end;

          end;

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      :: original: T_0

      redefine

      :: TSP_1:def7

      attr X is T_0 means for x,y be Point of X st x <> y & x in ( Cl {y}) holds not ( Cl {y}) c= ( Cl {x});

      compatibility

      proof

        thus X is T_0 implies for x,y be Point of X st x <> y & x in ( Cl {y}) holds not ( Cl {y}) c= ( Cl {x})

        proof

          assume

           A1: X is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x <> y;

            assume x in ( Cl {y});

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

            then ( Cl {x}) = ( Cl {y}) by A3, XBOOLE_0:def 10;

            hence contradiction by A1, A2;

          end;

        end;

        assume

         A4: for x,y be Point of X st x <> y & x in ( Cl {y}) holds not ( Cl {y}) c= ( Cl {x});

        for x,y be Point of X st x <> y holds not x in ( Cl {y}) or not y in ( Cl {x})

        proof

          let x,y be Point of X;

          assume

           A5: x <> y;

          assume

           A6: x in ( Cl {y});

          assume y in ( Cl {x});

          then {y} c= ( Cl {x}) by ZFMISC_1: 31;

          hence contradiction by A4, A5, A6, TOPS_1: 5;

        end;

        hence thesis;

      end;

    end

    registration

      cluster almost_discrete T_0 -> discrete for non empty TopSpace;

      coherence

      proof

        let Y be non empty TopSpace;

        assume

         A1: Y is almost_discrete T_0;

        for A be Subset of Y, x be Point of Y st A = {x} holds A is closed

        proof

          let A be Subset of Y, x be Point of Y;

          x in ( Cl {x}) by Lm2;

          then

           A2: {x} c= ( Cl {x}) by ZFMISC_1: 31;

           A3:

          now

            assume not ( Cl {x}) c= {x};

            then

            consider a be object such that

             A4: a in ( Cl {x}) and

             A5: not a in {x} by TARSKI:def 3;

            reconsider a as Point of Y by A4;

            a <> x by A5, TARSKI:def 1;

            then not x in ( Cl {a}) by A1, A4;

            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;

          end;

          assume A = {x};

          hence thesis by A2, A3, XBOOLE_0:def 10;

        end;

        hence thesis by A1, TDLAT_3: 26;

      end;

      cluster almost_discrete non discrete -> non T_0 for non empty TopSpace;

      coherence ;

      cluster non discrete T_0 -> non almost_discrete for non empty TopSpace;

      coherence ;

    end

    definition

      mode Kolmogorov_space is T_0 non empty TopSpace;

      mode non-Kolmogorov_space is non T_0 non empty TopSpace;

    end

    registration

      cluster non trivial strict for Kolmogorov_space;

      existence

      proof

        set X = the non trivial discrete strict non empty TopSpace;

        take X;

        thus thesis;

      end;

      cluster non trivial strict for non-Kolmogorov_space;

      existence

      proof

        set X = the non trivial anti-discrete strict non empty TopSpace;

        take X;

        thus thesis;

      end;

    end

    begin

    definition

      let Y be TopStruct;

      let IT be Subset of Y;

      :: TSP_1:def8

      attr IT is T_0 means for x,y be Point of Y st x in IT & y in IT & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W;

    end

    definition

      let Y be non empty TopStruct;

      let A be Subset of Y;

      :: original: T_0

      redefine

      :: TSP_1:def9

      attr A is T_0 means for x,y be Point of Y st x in A & y in A & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

      compatibility

      proof

        thus A is T_0 implies for x,y be Point of Y st x in A & y in A & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F

        proof

          assume

           A1: for x,y be Point of Y st x in A & y in A & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W;

          let x,y be Point of Y;

          assume

           A2: x in A & y in A & x <> y;

          hereby

            per cases by A1, A2;

              suppose ex V be Subset of Y st V is open & x in V & not y in V;

              then

              consider V be Subset of Y such that

               A3: V is open and

               A4: x in V and

               A5: not y in V;

              now

                take F = (V ` );

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

                hence F is closed by A3, PRE_TOPC:def 3;

                thus not x in F by A4, XBOOLE_0:def 5;

                thus y in F by A5, SUBSET_1: 29;

              end;

              hence thesis;

            end;

              suppose ex W be Subset of Y st W is open & not x in W & y in W;

              then

              consider W be Subset of Y such that

               A6: W is open and

               A7: not x in W and

               A8: y in W;

              now

                take E = (W ` );

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

                hence E is closed by A6, PRE_TOPC:def 3;

                thus x in E by A7, SUBSET_1: 29;

                thus not y in E by A8, XBOOLE_0:def 5;

              end;

              hence thesis;

            end;

          end;

        end;

        assume

         A9: for x,y be Point of Y st x in A & y in A & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

        for x,y be Point of Y st x in A & y in A & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W

        proof

          let x,y be Point of Y;

          assume

           A10: x in A & y in A & x <> y;

          hereby

            per cases by A9, A10;

              suppose ex E be Subset of Y st E is closed & x in E & not y in E;

              then

              consider E be Subset of Y such that

               A11: E is closed and

               A12: x in E and

               A13: not y in E;

              now

                take W = (E ` );

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

                hence W is open by A11, PRE_TOPC:def 3;

                thus not x in W by A12, XBOOLE_0:def 5;

                thus y in W by A13, SUBSET_1: 29;

              end;

              hence thesis;

            end;

              suppose ex F be Subset of Y st F is closed & not x in F & y in F;

              then

              consider F be Subset of Y such that

               A14: F is closed and

               A15: not x in F and

               A16: y in F;

              now

                take V = (F ` );

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

                hence V is open by A14, PRE_TOPC:def 3;

                thus x in V by A15, SUBSET_1: 29;

                thus not y in V by A16, XBOOLE_0:def 5;

              end;

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: TSP_1:3

    for Y0,Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is T_0 implies D1 is T_0

    proof

      let Y0,Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1;

      assume

       A1: the TopStruct of Y0 = the TopStruct of Y1;

      assume

       A2: D0 = D1;

      assume

       A3: D0 is T_0;

      now

        let x,y be Point of Y1;

        reconsider x0 = x, y0 = y as Point of Y0 by A1;

        assume

         A4: x in D1 & y in D1;

        assume

         A5: x <> y;

        hereby

          per cases by A2, A3, A4, A5;

            suppose ex V be Subset of Y0 st V is open & x0 in V & not y0 in V;

            then

            consider V be 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

              take V1;

              V1 in the topology of Y1 by A1, A6, PRE_TOPC:def 2;

              hence V1 is open by PRE_TOPC:def 2;

              thus x in V1 & not y in V1 by A7;

            end;

            hence (ex V1 be Subset of Y1 st V1 is open & x in V1 & not y in V1) or ex W1 be Subset of Y1 st W1 is open & not x in W1 & y in W1;

          end;

            suppose ex W be Subset of Y0 st W is open & not x0 in W & y0 in W;

            then

            consider W be 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

              take W1;

              W1 in the topology of Y1 by A1, A8, PRE_TOPC:def 2;

              hence W1 is open by PRE_TOPC:def 2;

              thus not x in W1 & y in W1 by A9;

            end;

            hence (ex V1 be Subset of Y1 st V1 is open & x in V1 & not y in V1) or ex W1 be Subset of Y1 st W1 is open & not x in W1 & y in W1;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: TSP_1:4

    

     Th4: for Y be non empty TopStruct, A be Subset of Y st A = the carrier of Y holds A is T_0 iff Y is T_0;

    reserve Y for non empty TopStruct;

    theorem :: TSP_1:5

    

     Th5: for A,B be Subset of Y st B c= A holds A is T_0 implies B is T_0;

    theorem :: TSP_1:6

    

     Th6: for A,B be Subset of Y holds A is T_0 or B is T_0 implies (A /\ B) is T_0

    proof

      let A,B be Subset of Y;

      assume

       A1: A is T_0 or B is T_0;

      hereby

        per cases by A1;

          suppose A is T_0;

          hence thesis by Th5, XBOOLE_1: 17;

        end;

          suppose B is T_0;

          hence thesis by Th5, XBOOLE_1: 17;

        end;

      end;

    end;

    theorem :: TSP_1:7

    

     Th7: for A,B be Subset of Y st A is open or B is open holds A is T_0 & B is T_0 implies (A \/ B) is T_0

    proof

      let A,B be Subset of Y;

      assume

       A1: A is open or B is open;

      assume that

       A2: A is T_0 and

       A3: B is T_0;

      now

        let x,y be Point of Y;

        assume

         A4: x in (A \/ B) & y in (A \/ B);

        then

         A5: x in ((A \ B) \/ B) & y in ((A \ B) \/ B) by XBOOLE_1: 39;

        assume

         A6: x <> y;

        

         A7: x in (A \/ (B \ A)) & y in (A \/ (B \ A)) by A4, XBOOLE_1: 39;

        now

          per cases by A1;

            suppose

             A8: A is open;

            now

              per cases by A7, XBOOLE_0:def 3;

                suppose x in A & y in A;

                hence (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W by A2, A6;

              end;

                suppose

                 A9: x in A & y in (B \ A);

                now

                  take A;

                  thus A is open by A8;

                  thus x in A by A9;

                  thus not y in A by A9, XBOOLE_0:def 5;

                end;

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

              end;

                suppose

                 A10: x in (B \ A) & y in A;

                now

                  take A;

                  thus A is open by A8;

                  thus not x in A by A10, XBOOLE_0:def 5;

                  thus y in A by A10;

                end;

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

              end;

                suppose

                 A11: x in (B \ A) & y in (B \ A);

                (B \ A) c= B by XBOOLE_1: 36;

                hence (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W by A3, A6, A11;

              end;

            end;

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

          end;

            suppose

             A12: B is open;

            now

              per cases by A5, XBOOLE_0:def 3;

                suppose

                 A13: x in (A \ B) & y in (A \ B);

                (A \ B) c= A by XBOOLE_1: 36;

                hence (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W by A2, A6, A13;

              end;

                suppose

                 A14: x in (A \ B) & y in B;

                now

                  take B;

                  thus B is open by A12;

                  thus not x in B by A14, XBOOLE_0:def 5;

                  thus y in B by A14;

                end;

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

              end;

                suppose

                 A15: x in B & y in (A \ B);

                now

                  take B;

                  thus B is open by A12;

                  thus x in B by A15;

                  thus not y in B by A15, XBOOLE_0:def 5;

                end;

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

              end;

                suppose x in B & y in B;

                hence (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W by A3, A6;

              end;

            end;

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

          end;

        end;

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

      end;

      hence thesis;

    end;

    theorem :: TSP_1:8

    

     Th8: for A,B be Subset of Y st A is closed or B is closed holds A is T_0 & B is T_0 implies (A \/ B) is T_0

    proof

      let A,B be Subset of Y;

      assume

       A1: A is closed or B is closed;

      assume that

       A2: A is T_0 and

       A3: B is T_0;

      now

        let x,y be Point of Y;

        assume

         A4: x in (A \/ B) & y in (A \/ B);

        then

         A5: x in ((A \ B) \/ B) & y in ((A \ B) \/ B) by XBOOLE_1: 39;

        assume

         A6: x <> y;

        

         A7: x in (A \/ (B \ A)) & y in (A \/ (B \ A)) by A4, XBOOLE_1: 39;

        now

          per cases by A1;

            suppose

             A8: A is closed;

            now

              per cases by A7, XBOOLE_0:def 3;

                suppose x in A & y in A;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W by A2, A6;

              end;

                suppose

                 A9: x in A & y in (B \ A);

                now

                  take A;

                  thus A is closed by A8;

                  thus x in A by A9;

                  thus not y in A by A9, XBOOLE_0:def 5;

                end;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

              end;

                suppose

                 A10: x in (B \ A) & y in A;

                now

                  take A;

                  thus A is closed by A8;

                  thus not x in A by A10, XBOOLE_0:def 5;

                  thus y in A by A10;

                end;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

              end;

                suppose

                 A11: x in (B \ A) & y in (B \ A);

                (B \ A) c= B by XBOOLE_1: 36;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W by A3, A6, A11;

              end;

            end;

            hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

          end;

            suppose

             A12: B is closed;

            now

              per cases by A5, XBOOLE_0:def 3;

                suppose

                 A13: x in (A \ B) & y in (A \ B);

                (A \ B) c= A by XBOOLE_1: 36;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W by A2, A6, A13;

              end;

                suppose

                 A14: x in (A \ B) & y in B;

                now

                  take B;

                  thus B is closed by A12;

                  thus not x in B by A14, XBOOLE_0:def 5;

                  thus y in B by A14;

                end;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

              end;

                suppose

                 A15: x in B & y in (A \ B);

                now

                  take B;

                  thus B is closed by A12;

                  thus x in B by A15;

                  thus not y in B by A15, XBOOLE_0:def 5;

                end;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

              end;

                suppose x in B & y in B;

                hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W by A3, A6;

              end;

            end;

            hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

          end;

        end;

        hence (ex V be Subset of Y st V is closed & x in V & not y in V) or ex W be Subset of Y st W is closed & not x in W & y in W;

      end;

      hence thesis;

    end;

    theorem :: TSP_1:9

    

     Th9: for A be Subset of Y holds A is discrete implies A is T_0

    proof

      let A be Subset of Y;

      assume

       A1: A is discrete;

      now

        let x,y be Point of Y;

        assume that

         A2: x in A and

         A3: y in A;

         {x} c= A by A2, ZFMISC_1: 31;

        then

        consider G be Subset of Y such that

         A4: G is open and

         A5: (A /\ G) = {x} by A1, TEX_2:def 3;

        assume

         A6: x <> y;

        now

          take G;

          thus G is open by A4;

          x in {x} by TARSKI:def 1;

          hence x in G by A5, XBOOLE_0:def 4;

          now

            assume y in G;

            then y in {x} by A3, A5, XBOOLE_0:def 4;

            hence contradiction by A6, TARSKI:def 1;

          end;

          hence not y in G;

        end;

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

      end;

      hence thesis;

    end;

    theorem :: TSP_1:10

    for A be non empty Subset of Y holds A is anti-discrete & not A is trivial implies not A is T_0

    proof

      let A be non empty Subset of Y;

      assume

       A1: A is anti-discrete;

      consider s be object 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;

      then A <> {s0};

      then

      consider t be object such that

       A3: t in A and

       A4: t <> s0 by ZFMISC_1: 35;

      reconsider s, t as Point of Y by A2, A3;

      assume

       A5: A is T_0;

      now

        per cases by A3, A4, A5;

          suppose ex E be Subset of Y st E is closed & s in E & not t in E;

          then

          consider E be 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;

        end;

          suppose ex F be Subset of Y st F is closed & not s in F & t in F;

          then

          consider F be 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;

        end;

      end;

      hence contradiction;

    end;

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_1:def10

      attr A is T_0 means for x,y be Point of X st x in A & y in A & x <> y holds ( Cl {x}) <> ( Cl {y});

      compatibility

      proof

        thus A is T_0 implies for x,y be Point of X st x in A & y in A & x <> y holds ( Cl {x}) <> ( Cl {y})

        proof

          assume

           A1: A is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x in A & y in A & x <> y;

            now

              per cases by A1, A2;

                suppose ex V be Subset of X st V is open & x in V & not y in V;

                then

                consider V be 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});

                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;

              end;

                suppose ex W be Subset of X st W is open & not x in W & y in W;

                then

                consider W be 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});

                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;

              end;

            end;

            hence ( Cl {x}) <> ( Cl {y});

          end;

        end;

        assume

         A13: for x,y be Point of X st x in A & y in A & x <> y holds ( Cl {x}) <> ( Cl {y});

        now

          let x,y be Point of X;

          assume

           A14: x in A & y in A & x <> y;

          assume

           A15: for E be Subset of X st E is closed & x in E holds y in E;

          thus ex F be Subset of X st F is closed & not x in F & y in F

          proof

            set F = ( Cl {y});

            take F;

            thus F is closed;

            now

              assume x in F;

              then {x} c= F by ZFMISC_1: 31;

              then

               A16: ( Cl {x}) c= F by TOPS_1: 5;

              y in ( Cl {x}) by A15, Lm2;

              then {y} c= ( Cl {x}) by ZFMISC_1: 31;

              then F c= ( Cl {x}) by TOPS_1: 5;

              then ( Cl {x}) = F by A16, XBOOLE_0:def 10;

              hence contradiction by A13, A14;

            end;

            hence not x in F;

            thus thesis by Lm2;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_1:def11

      attr A is T_0 means for x,y be Point of X st x in A & y in A & x <> y holds not x in ( Cl {y}) or not y in ( Cl {x});

      compatibility

      proof

        thus A is T_0 implies for x,y be Point of X st x in A & y in A & x <> y holds not x in ( Cl {y}) or not y in ( Cl {x})

        proof

          assume

           A1: A is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x in A & y in A & x <> y;

            assume that

             A3: x in ( Cl {y}) and

             A4: y in ( Cl {x});

             {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;

          end;

        end;

        assume

         A6: for x,y be Point of X st x in A & y in A & x <> y holds not x in ( Cl {y}) or not y in ( Cl {x});

        for x,y be 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;

          assume

           A7: x in A & y in A & x <> y;

          assume

           A8: ( Cl {x}) = ( Cl {y});

          now

            per cases by A6, A7;

              suppose not x in ( Cl {y});

              hence contradiction by A8, Lm2;

            end;

              suppose not y in ( Cl {x});

              hence contradiction by A8, Lm2;

            end;

          end;

          hence contradiction;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_1:def12

      attr A is T_0 means for x,y be Point of X st x in A & y in A & x <> y holds x in ( Cl {y}) implies not ( Cl {y}) c= ( Cl {x});

      compatibility

      proof

        thus A is T_0 implies for x,y be Point of X st x in A & y in A & x <> y holds x in ( Cl {y}) implies not ( Cl {y}) c= ( Cl {x})

        proof

          assume

           A1: A is T_0;

          hereby

            let x,y be Point of X;

            assume

             A2: x in A & y in A & x <> y;

            assume x in ( Cl {y});

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

            then ( Cl {x}) = ( Cl {y}) by A3, XBOOLE_0:def 10;

            hence contradiction by A1, A2;

          end;

        end;

        assume

         A4: for x,y be Point of X st x in A & y in A & x <> y holds x in ( Cl {y}) implies not ( Cl {y}) c= ( Cl {x});

        for x,y be Point of X st x in A & y in A & x <> y holds not x in ( Cl {y}) or not y in ( Cl {x})

        proof

          let x,y be Point of X;

          assume

           A5: x in A & y in A & x <> y;

          assume

           A6: x in ( Cl {y});

          assume y in ( Cl {x});

          then {y} c= ( Cl {x}) by ZFMISC_1: 31;

          hence contradiction by A4, A5, A6, TOPS_1: 5;

        end;

        hence thesis;

      end;

    end

    reserve X for non empty TopSpace;

    theorem :: TSP_1:11

    for A be empty Subset of X holds A is T_0;

    theorem :: TSP_1:12

    for x be Point of X holds {x} is T_0 by Th9, TEX_2: 30;

    begin

    registration

      let Y be non empty TopStruct;

      cluster strict T_0 non empty for SubSpace of Y;

      existence

      proof

        set X0 = the trivial strict non empty SubSpace of Y;

        take X0;

        thus thesis;

      end;

    end

     Lm3:

    now

      let Z be TopStruct;

      let Z0 be SubSpace of Z;

      ( [#] Z0) c= ( [#] Z) by PRE_TOPC:def 4;

      hence the carrier of Z0 is Subset of Z;

    end;

    definition

      let Y be TopStruct;

      let Y0 be SubSpace of Y;

      :: original: T_0

      redefine

      :: TSP_1:def13

      attr Y0 is T_0 means Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W;

      compatibility

      proof

        reconsider A = the carrier of Y0 as Subset of Y by Lm3;

        thus Y0 is T_0 implies Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W

        proof

          assume

           A1: Y0 is T_0;

          hereby

            assume

             A2: Y0 is non empty;

            let x,y be Point of Y;

            assume x is Point of Y0 & y is Point of Y0;

            then

            reconsider x0 = x, y0 = y as Point of Y0;

            assume

             A3: x <> y;

            now

              per cases by A1, A2, A3;

                suppose ex E0 be Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0;

                then

                consider E0 be Subset of Y0 such that

                 A4: E0 is open and

                 A5: x0 in E0 and

                 A6: not y0 in E0;

                now

                  consider E be Subset of Y such that

                   A7: E is open and

                   A8: E0 = (E /\ A) by A4, Def1;

                  take E;

                  thus E is open by A7;

                  (E /\ A) c= E by XBOOLE_1: 17;

                  hence x in E by A5, A8;

                  thus not y in E by A2, A6, A8, XBOOLE_0:def 4;

                end;

                hence (ex E be Subset of Y st E is open & x in E & not y in E) or ex F be Subset of Y st F is open & not x in F & y in F;

              end;

                suppose ex F0 be Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;

                then

                consider F0 be Subset of Y0 such that

                 A9: F0 is open and

                 A10: not x0 in F0 and

                 A11: y0 in F0;

                now

                  consider F be Subset of Y such that

                   A12: F is open and

                   A13: F0 = (F /\ A) by A9, Def1;

                  take F;

                  thus F is open by A12;

                  thus not x in F by A2, A10, A13, XBOOLE_0:def 4;

                  (F /\ A) c= F by XBOOLE_1: 17;

                  hence y in F by A11, A13;

                end;

                hence (ex E be Subset of Y st E is open & x in E & not y in E) or ex F be Subset of Y st F is open & not x in F & y in F;

              end;

            end;

            hence (ex E be Subset of Y st E is open & x in E & not y in E) or ex F be Subset of Y st F is open & not x in F & y in F;

          end;

        end;

        assume

         A14: Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex V be Subset of Y st V is open & x in V & not y in V) or ex W be Subset of Y st W is open & not x in W & y in W;

        now

          

           A15: the carrier of Y0 c= the carrier of Y by Def1;

          assume

           A16: Y0 is non empty;

          let x0,y0 be Point of Y0;

          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;

          now

            per cases by A14, A16, A17;

              suppose ex E be Subset of Y st E is open & x in E & not y in E;

              then

              consider E be Subset of Y such that

               A18: E is open and

               A19: x in E and

               A20: not y in E;

              now

                consider E0 be Subset of Y0 such that

                 A21: E0 is open and

                 A22: E0 = (E /\ A) by A18, Th1;

                take E0;

                thus E0 is open by A21;

                thus x0 in E0 by A16, A19, A22, XBOOLE_0:def 4;

                now

                  

                   A23: (E /\ A) c= E by XBOOLE_1: 17;

                  assume y0 in E0;

                  hence contradiction by A20, A22, A23;

                end;

                hence not y0 in E0;

              end;

              hence (ex E0 be Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;

            end;

              suppose ex F be Subset of Y st F is open & not x in F & y in F;

              then

              consider F be Subset of Y such that

               A24: F is open and

               A25: not x in F and

               A26: y in F;

              now

                consider F0 be Subset of Y0 such that

                 A27: F0 is open and

                 A28: F0 = (F /\ A) by A24, Th1;

                take F0;

                thus F0 is open by A27;

                now

                  

                   A29: (F /\ A) c= F by XBOOLE_1: 17;

                  assume x0 in F0;

                  hence contradiction by A25, A28, A29;

                end;

                hence not x0 in F0;

                thus y0 in F0 by A16, A26, A28, XBOOLE_0:def 4;

              end;

              hence (ex E0 be Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;

            end;

          end;

          hence (ex E0 be Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;

        end;

        hence thesis;

      end;

    end

    definition

      let Y be TopStruct;

      let Y0 be SubSpace of Y;

      :: original: T_0

      redefine

      :: TSP_1:def14

      attr Y0 is T_0 means Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

      compatibility

      proof

        reconsider A = the carrier of Y0 as Subset of Y by Lm3;

        thus Y0 is T_0 implies Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F

        proof

          assume

           A1: Y0 is T_0;

          hereby

            assume

             A2: not Y0 is empty;

            let x,y be Point of Y;

            assume x is Point of Y0 & y is Point of Y0;

            then

            reconsider x0 = x, y0 = y as Point of Y0;

            assume

             A3: x <> y;

            now

              per cases by A1, A2, A3;

                suppose ex E0 be Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0;

                then

                consider E0 be Subset of Y0 such that

                 A4: E0 is closed and

                 A5: x0 in E0 and

                 A6: not y0 in E0;

                now

                  consider E be Subset of Y such that

                   A7: E is closed and

                   A8: E0 = (E /\ A) by A4, Def2;

                  take E;

                  thus E is closed by A7;

                  (E /\ A) c= E by XBOOLE_1: 17;

                  hence x in E by A5, A8;

                  thus not y in E by A2, A6, A8, XBOOLE_0:def 4;

                end;

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

              end;

                suppose ex F0 be Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;

                then

                consider F0 be Subset of Y0 such that

                 A9: F0 is closed and

                 A10: not x0 in F0 and

                 A11: y0 in F0;

                now

                  consider F be Subset of Y such that

                   A12: F is closed and

                   A13: F0 = (F /\ A) by A9, Def2;

                  take F;

                  thus F is closed by A12;

                  thus not x in F by A2, A10, A13, XBOOLE_0:def 4;

                  (F /\ A) c= F by XBOOLE_1: 17;

                  hence y in F by A11, A13;

                end;

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

              end;

            end;

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

          end;

        end;

        assume

         A14: Y0 is empty or for x,y be Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E be Subset of Y st E is closed & x in E & not y in E) or ex F be Subset of Y st F is closed & not x in F & y in F;

        now

          

           A15: the carrier of Y0 c= the carrier of Y by Def1;

          assume

           A16: not Y0 is empty;

          let x0,y0 be Point of Y0;

          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;

          now

            per cases by A14, A16, A17;

              suppose ex E be Subset of Y st E is closed & x in E & not y in E;

              then

              consider E be Subset of Y such that

               A18: E is closed and

               A19: x in E and

               A20: not y in E;

              now

                consider E0 be Subset of Y0 such that

                 A21: E0 is closed and

                 A22: E0 = (E /\ A) by A18, Th2;

                take E0;

                thus E0 is closed by A21;

                thus x0 in E0 by A16, A19, A22, XBOOLE_0:def 4;

                now

                  

                   A23: (E /\ A) c= E by XBOOLE_1: 17;

                  assume y0 in E0;

                  hence contradiction by A20, A22, A23;

                end;

                hence not y0 in E0;

              end;

              hence (ex E0 be Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;

            end;

              suppose ex F be Subset of Y st F is closed & not x in F & y in F;

              then

              consider F be Subset of Y such that

               A24: F is closed and

               A25: not x in F and

               A26: y in F;

              now

                consider F0 be Subset of Y0 such that

                 A27: F0 is closed and

                 A28: F0 = (F /\ A) by A24, Th2;

                take F0;

                thus F0 is closed by A27;

                now

                  

                   A29: (F /\ A) c= F by XBOOLE_1: 17;

                  assume x0 in F0;

                  hence contradiction by A25, A28, A29;

                end;

                hence not x0 in F0;

                thus y0 in F0 by A16, A26, A28, XBOOLE_0:def 4;

              end;

              hence (ex E0 be Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;

            end;

          end;

          hence (ex E0 be Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0) or ex F0 be Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;

        end;

        hence thesis;

      end;

    end

    reserve Y for non empty TopStruct;

    theorem :: TSP_1:13

    

     Th13: for Y0 be non empty SubSpace of Y, A be Subset of Y st A = the carrier of Y0 holds A is T_0 iff Y0 is T_0;

    theorem :: TSP_1:14

    for Y0 be non empty SubSpace of Y, Y1 be T_0 non empty SubSpace of Y st Y0 is SubSpace of Y1 holds Y0 is T_0

    proof

      let Y0 be non empty SubSpace of Y, Y1 be T_0 non empty SubSpace of Y;

      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;

      

       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;

      hence thesis;

    end;

    reserve X for non empty TopSpace;

    theorem :: TSP_1:15

    for X1 be T_0 non empty SubSpace of X, X2 be non empty SubSpace of X holds X1 meets X2 implies (X1 meet X2) is T_0

    proof

      let X1 be T_0 non empty SubSpace of X, X2 be non empty SubSpace of X;

      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;

      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 thesis by A1;

    end;

    theorem :: TSP_1:16

    for X1,X2 be T_0 non empty SubSpace of X holds X1 is open or X2 is open implies (X1 union X2) is T_0

    proof

      let X1,X2 be T_0 non empty SubSpace of X;

      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;

      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 thesis;

    end;

    theorem :: TSP_1:17

    for X1,X2 be T_0 non empty SubSpace of X holds X1 is closed or X2 is closed implies (X1 union X2) is T_0

    proof

      let X1,X2 be T_0 non empty SubSpace of X;

      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;

      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 thesis;

    end;

    definition

      let X be non empty TopSpace;

      mode Kolmogorov_subspace of X is T_0 non empty SubSpace of X;

    end

    theorem :: TSP_1:18

    for X be non empty TopSpace, A0 be non empty Subset of X st A0 is T_0 holds ex X0 be strict Kolmogorov_subspace of X st A0 = the carrier of X0

    proof

      let X be non empty TopSpace, A0 be non empty Subset of X;

      consider X0 be strict non empty SubSpace of X such that

       A1: A0 = the carrier of X0 by TSEP_1: 10;

      assume A0 is T_0;

      then

      reconsider X0 as strict Kolmogorov_subspace of X by A1, Th13;

      take X0;

      thus thesis by A1;

    end;

    registration

      let X be non trivial TopSpace;

      cluster proper strict for Kolmogorov_subspace of X;

      existence

      proof

        set X0 = the trivial strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be Kolmogorov_space;

      cluster -> T_0 for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        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;

        hence thesis;

      end;

    end

    registration

      let X be non-Kolmogorov_space;

      cluster non proper -> non T_0 for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

        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 X0 is non proper;

        then not A0 is proper by TEX_2: 8;

        then A0 = A;

        then not A0 is T_0 by Th4;

        hence thesis;

      end;

      cluster T_0 -> proper for non empty SubSpace of X;

      coherence ;

    end

    registration

      let X be non-Kolmogorov_space;

      cluster strict non T_0 for SubSpace of X;

      existence

      proof

        set X0 = the non proper strict non empty SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    definition

      let X be non-Kolmogorov_space;

      mode non-Kolmogorov_subspace of X is non T_0 SubSpace of X;

    end

    theorem :: TSP_1:19

    for X be non empty non-Kolmogorov_space, A0 be Subset of X st not A0 is T_0 holds ex X0 be strict non-Kolmogorov_subspace of X st A0 = the carrier of X0

    proof

      let X be non empty non-Kolmogorov_space, A0 be Subset of X;

      assume

       A1: not A0 is T_0;

      then A0 is non empty;

      then

      consider X0 be strict non empty SubSpace of X such that

       A2: A0 = the carrier of X0 by TSEP_1: 10;

      reconsider X0 as non T_0 strict SubSpace of X by A1, A2, Th13;

      take X0;

      thus thesis by A2;

    end;