tsp_2.miz

    begin

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_2:def1

      attr A is T_0 means for a,b be Point of X st a in A & b in A holds a <> b implies ( MaxADSet a) misses ( MaxADSet b);

      compatibility

      proof

        thus A is T_0 implies for a,b be Point of X st a in A & b in A holds a <> b implies ( MaxADSet a) misses ( MaxADSet b)

        proof

          assume

           A1: A is T_0;

          let a,b be Point of X;

          assume that

           A2: a in A and

           A3: b in A;

          assume

           A4: a <> b;

          now

            per cases by A1, A2, A3, A4, TSP_1:def 8;

              suppose ex V be Subset of X st V is open & a in V & not b in V;

              then

              consider V be Subset of X such that

               A5: V is open and

               A6: a in V and

               A7: not b in V;

              now

                take V;

                thus V is open by A5;

                thus ( MaxADSet a) c= V by A5, A6, TEX_4: 24;

                b in (( [#] X) \ V) by A7, XBOOLE_0:def 5;

                then ( MaxADSet b) c= (V ` ) by A5, TEX_4: 23;

                hence V misses ( MaxADSet b) by SUBSET_1: 23;

              end;

              hence (ex V be Subset of X st V is open & ( MaxADSet a) c= V & V misses ( MaxADSet b)) or ex W be Subset of X st W is open & W misses ( MaxADSet a) & ( MaxADSet b) c= W;

            end;

              suppose ex W be Subset of X st W is open & not a in W & b in W;

              then

              consider W be Subset of X such that

               A8: W is open and

               A9: not a in W and

               A10: b in W;

              now

                take W;

                thus W is open by A8;

                a in (( [#] X) \ W) by A9, XBOOLE_0:def 5;

                then ( MaxADSet a) c= (W ` ) by A8, TEX_4: 23;

                hence W misses ( MaxADSet a) by SUBSET_1: 23;

                thus ( MaxADSet b) c= W by A8, A10, TEX_4: 24;

              end;

              hence (ex V be Subset of X st V is open & ( MaxADSet a) c= V & V misses ( MaxADSet b)) or ex W be Subset of X st W is open & W misses ( MaxADSet a) & ( MaxADSet b) c= W;

            end;

          end;

          hence thesis by TEX_4: 53;

        end;

        assume

         A11: for a,b be Point of X st a in A & b in A holds a <> b implies ( MaxADSet a) misses ( MaxADSet b);

        now

          let a,b be Point of X;

          assume that

           A12: a in A and

           A13: b in A;

          assume a <> b;

          then

           A14: ( MaxADSet a) misses ( MaxADSet b) by A11, A12, A13;

          now

            per cases by A14, TEX_4: 53;

              suppose ex V be Subset of X st V is open & ( MaxADSet a) c= V & V misses ( MaxADSet b);

              then

              consider V be Subset of X such that

               A15: V is open and

               A16: ( MaxADSet a) c= V and

               A17: V misses ( MaxADSet b);

              now

                take V;

                thus V is open by A15;

                 {a} c= ( MaxADSet a) by TEX_4: 18;

                then a in ( MaxADSet a) by ZFMISC_1: 31;

                hence a in V by A16;

                now

                   {b} c= ( MaxADSet b) by TEX_4: 18;

                  then

                   A18: b in ( MaxADSet b) by ZFMISC_1: 31;

                  assume b in V;

                  hence contradiction by A17, A18, XBOOLE_0: 3;

                end;

                hence not b in V;

              end;

              hence (ex V be Subset of X st V is open & a in V & not b in V) or ex W be Subset of X st W is open & not a in W & b in W;

            end;

              suppose ex W be Subset of X st W is open & W misses ( MaxADSet a) & ( MaxADSet b) c= W;

              then

              consider W be Subset of X such that

               A19: W is open and

               A20: W misses ( MaxADSet a) and

               A21: ( MaxADSet b) c= W;

              now

                take W;

                thus W is open by A19;

                now

                   {a} c= ( MaxADSet a) by TEX_4: 18;

                  then

                   A22: a in ( MaxADSet a) by ZFMISC_1: 31;

                  assume a in W;

                  hence contradiction by A20, A22, XBOOLE_0: 3;

                end;

                hence not a in W;

                 {b} c= ( MaxADSet b) by TEX_4: 18;

                then b in ( MaxADSet b) by ZFMISC_1: 31;

                hence b in W by A21;

              end;

              hence (ex V be Subset of X st V is open & a in V & not b in V) or ex W be Subset of X st W is open & not a in W & b in W;

            end;

          end;

          hence (ex V be Subset of X st V is open & a in V & not b in V) or ex W be Subset of X st W is open & not a in W & b in W;

        end;

        hence thesis by TSP_1:def 8;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_2:def2

      attr A is T_0 means for a be Point of X st a in A holds (A /\ ( MaxADSet a)) = {a};

      compatibility

      proof

        thus A is T_0 implies for a be Point of X st a in A holds (A /\ ( MaxADSet a)) = {a}

        proof

          assume

           A1: A is T_0;

          let a be Point of X;

          assume

           A2: a in A;

          assume

           A3: (A /\ ( MaxADSet a)) <> {a};

           {a} c= ( MaxADSet a) by TEX_4: 18;

          then a in ( MaxADSet a) by ZFMISC_1: 31;

          then a in (A /\ ( MaxADSet a)) by A2, XBOOLE_0:def 4;

          then

          consider b be object such that

           A4: b in (A /\ ( MaxADSet a)) and

           A5: b <> a by A3, ZFMISC_1: 35;

          reconsider b as Point of X by A4;

          b in A by A4, XBOOLE_0:def 4;

          then

           A6: ( MaxADSet a) misses ( MaxADSet b) by A1, A2, A5;

          b in ( MaxADSet a) by A4, XBOOLE_0:def 4;

          hence contradiction by A6, TEX_4: 21;

        end;

        assume

         A7: for a be Point of X st a in A holds (A /\ ( MaxADSet a)) = {a};

        now

          let a,b be Point of X;

          assume that

           A8: a in A and

           A9: b in A;



           A10: (A /\ ( MaxADSet a)) = {a} by A7, A8;



           A11: (A /\ ( MaxADSet b)) = {b} by A7, A9;

          assume

           A12: a <> b;

          assume ( MaxADSet a) meets ( MaxADSet b);

          then {a} = {b} by A10, A11, TEX_4: 22;

          hence contradiction by A12, ZFMISC_1: 3;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty TopSpace;

      let A be Subset of X;

      :: original: T_0

      redefine

      :: TSP_2:def3

      attr A is T_0 means for a be Point of X st a in A holds ex D be Subset of X st D is maximal_anti-discrete & (A /\ D) = {a};

      compatibility

      proof

        thus A is T_0 implies for a be Point of X st a in A holds ex D be Subset of X st D is maximal_anti-discrete & (A /\ D) = {a}

        proof

          assume

           A1: A is T_0;

          let a be Point of X;

          assume

           A2: a in A;

          take D = ( MaxADSet a);

          thus D is maximal_anti-discrete by TEX_4: 20;

          thus thesis by A1, A2;

        end;

        assume

         A3: for a be Point of X st a in A holds ex D be Subset of X st D is maximal_anti-discrete & (A /\ D) = {a};

        now

          let a be Point of X;

          assume a in A;

          then

          consider D be Subset of X such that

           A4: D is maximal_anti-discrete and

           A5: (A /\ D) = {a} by A3;

          a in (A /\ D) by A5, ZFMISC_1: 31;

          then a in D by XBOOLE_0:def 4;

          hence (A /\ ( MaxADSet a)) = {a} by A4, A5, TEX_4: 27;

        end;

        hence thesis;

      end;

    end

    definition

      let Y be TopStruct;

      let IT be Subset of Y;

      :: TSP_2:def4

      attr IT is maximal_T_0 means IT is T_0 & for D be Subset of Y st D is T_0 & IT c= D holds IT = D;

    end

    theorem :: TSP_2:1

    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 maximal_T_0 implies D1 is maximal_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 maximal_T_0;

       A4:

      now

        let D be Subset of Y1;

        reconsider E = D as Subset of Y0 by A1;

        assume D is T_0;

        then

         A5: E is T_0 by A1, TSP_1: 3;

        assume D1 c= D;

        hence D1 = D by A2, A3, A5;

      end;

      D0 is T_0 by A3;

      then D1 is T_0 by A1, A2, TSP_1: 3;

      hence thesis by A4;

    end;

    definition

      let X be non empty TopSpace;

      let M be Subset of X;

      :: original: maximal_T_0

      redefine

      :: TSP_2:def5

      attr M is maximal_T_0 means M is T_0 & ( MaxADSet M) = the carrier of X;

      compatibility

      proof

        thus M is maximal_T_0 implies M is T_0 & ( MaxADSet M) = the carrier of X

        proof

          assume

           A1: M is maximal_T_0;

          hence

           A2: M is T_0;

          the carrier of X c= ( MaxADSet M)

          proof

            assume not the carrier of X c= ( MaxADSet M);

            then

            consider x be object such that

             A3: x in the carrier of X and

             A4: not x in ( MaxADSet M) by TARSKI:def 3;

            reconsider x as Point of X by A3;

            set A = (M \/ {x});

            for a be Point of X st a in A holds (A /\ ( MaxADSet a)) = {a}

            proof

              let a be Point of X;

              assume a in A;

              then

               A5: a in M or a in {x} by XBOOLE_0:def 3;

              now

                per cases by A5, TARSKI:def 1;

                  suppose

                   A6: a in M;

                  ( {x} /\ ( MaxADSet a)) = {}

                  proof

                    assume ( {x} /\ ( MaxADSet a)) <> {} ;

                    then {x} meets ( MaxADSet a) by XBOOLE_0:def 7;

                    then

                     A7: x in ( MaxADSet a) by ZFMISC_1: 50;

                     {a} c= M by A6, ZFMISC_1: 31;

                    then ( MaxADSet {a}) c= ( MaxADSet M) by TEX_4: 31;

                    then ( MaxADSet a) c= ( MaxADSet M) by TEX_4: 28;

                    hence contradiction by A4, A7;

                  end;



                  then (A /\ ( MaxADSet a)) = ((M /\ ( MaxADSet a)) \/ {} ) by XBOOLE_1: 23

                  .= (M /\ ( MaxADSet a));

                  hence thesis by A2, A6;

                end;

                  suppose

                   A8: a = x;

                  then

                   A9: {x} c= ( MaxADSet a) by TEX_4: 18;

                  (M /\ ( MaxADSet a)) = {}

                  proof



                     A10: M c= ( MaxADSet M) by TEX_4: 32;

                    assume (M /\ ( MaxADSet a)) <> {} ;

                    then (( MaxADSet a) /\ ( MaxADSet M)) <> {} by A10, XBOOLE_1: 3, XBOOLE_1: 26;

                    then ( MaxADSet a) meets ( MaxADSet M) by XBOOLE_0:def 7;

                    then

                     A11: ( MaxADSet a) c= ( MaxADSet M) by TEX_4: 30;

                    x in ( MaxADSet a) by A9, ZFMISC_1: 31;

                    hence contradiction by A4, A11;

                  end;



                  then (A /\ ( MaxADSet a)) = ( {} \/ ( {x} /\ ( MaxADSet a))) by XBOOLE_1: 23

                  .= ( {x} /\ ( MaxADSet a));

                  hence thesis by A8, TEX_4: 18, XBOOLE_1: 28;

                end;

              end;

              hence thesis;

            end;

            then

             A12: A is T_0;



             A13: M c= ( MaxADSet M) by TEX_4: 32;



             A14: {x} c= A by XBOOLE_1: 7;

            M c= A by XBOOLE_1: 7;

            then M = A by A1, A12;

            then x in M by A14, ZFMISC_1: 31;

            hence contradiction by A4, A13;

          end;

          hence thesis by XBOOLE_0:def 10;

        end;

        assume

         A15: M is T_0;

        assume

         A16: ( MaxADSet M) = the carrier of X;

        for D be Subset of X st D is T_0 & M c= D holds M = D

        proof

          let D be Subset of X;

          assume

           A17: D is T_0;

          assume

           A18: M c= D;

          D c= M

          proof

            assume not D c= M;

            then

            consider x be object such that

             A19: x in D and

             A20: not x in M by TARSKI:def 3;



             A21: x in the carrier of X by A19;

            reconsider x as Point of X by A19;

            x in ( union { ( MaxADSet a) where a be Point of X : a in M }) by A16, A21, TEX_4:def 11;

            then

            consider C be set such that

             A22: x in C and

             A23: C in { ( MaxADSet a) where a be Point of X : a in M } by TARSKI:def 4;

            consider a be Point of X such that

             A24: C = ( MaxADSet a) and

             A25: a in M by A23;

            (M /\ ( MaxADSet x)) c= (D /\ ( MaxADSet x)) by A18, XBOOLE_1: 26;

            then

             A26: (M /\ ( MaxADSet x)) c= {x} by A17, A19;

            ( MaxADSet a) = ( MaxADSet x) by A22, A24, TEX_4: 21;

            then (M /\ ( MaxADSet x)) = {a} by A15, A25;

            hence contradiction by A20, A25, A26, ZFMISC_1: 18;

          end;

          hence thesis by A18, XBOOLE_0:def 10;

        end;

        hence thesis by A15;

      end;

    end

    reserve X for non empty TopSpace;

    theorem :: TSP_2:2



     Th2: for M be Subset of X holds M is maximal_T_0 implies M is dense

    proof

      let M be Subset of X;

      assume

       A1: M is maximal_T_0;

      then ( MaxADSet M) = ( [#] X);

      then

       A2: ( Cl ( MaxADSet M)) = ( MaxADSet M) by PRE_TOPC: 22;

      ( MaxADSet M) = the carrier of X by A1;

      then ( Cl M) = the carrier of X by A2, TEX_4: 62;

      hence thesis by TOPS_3:def 2;

    end;

    theorem :: TSP_2:3



     Th3: for A be Subset of X st A is open or A is closed holds A is maximal_T_0 implies not A is proper by TEX_4: 56, TEX_4: 60;

    theorem :: TSP_2:4



     Th4: for A be empty Subset of X holds not A is maximal_T_0

    proof

      consider a be object such that

       A1: a in the carrier of X by XBOOLE_0:def 1;

      reconsider a as Point of X by A1;

      let A be empty Subset of X;

      now

        take C = {a};

        thus C is T_0 & A c= C & A <> C by TSP_1: 12, XBOOLE_1: 2;

      end;

      hence thesis;

    end;

    theorem :: TSP_2:5



     Th5: for M be Subset of X st M is maximal_T_0 holds for A be Subset of X st A is closed holds A = ( MaxADSet (M /\ A))

    proof

      let M be Subset of X;

      assume

       A1: M is maximal_T_0;

      let A be Subset of X;

      assume

       A2: A is closed;

      then ( MaxADSet (M /\ A)) = (( MaxADSet M) /\ ( MaxADSet A)) by TEX_4: 64;

      then

       A3: ( MaxADSet (M /\ A)) = (( MaxADSet M) /\ A) by A2, TEX_4: 60;

      A = (the carrier of X /\ A) by XBOOLE_1: 28;

      hence thesis by A1, A3;

    end;

    theorem :: TSP_2:6



     Th6: for M be Subset of X st M is maximal_T_0 holds for A be Subset of X st A is open holds A = ( MaxADSet (M /\ A))

    proof

      let M be Subset of X;

      assume

       A1: M is maximal_T_0;

      let A be Subset of X;

      assume

       A2: A is open;

      then ( MaxADSet (M /\ A)) = (( MaxADSet M) /\ ( MaxADSet A)) by TEX_4: 65;

      then

       A3: ( MaxADSet (M /\ A)) = (( MaxADSet M) /\ A) by A2, TEX_4: 56;

      A = (the carrier of X /\ A) by XBOOLE_1: 28;

      hence thesis by A1, A3;

    end;

    theorem :: TSP_2:7

    for M be Subset of X st M is maximal_T_0 holds for A be Subset of X holds ( Cl A) = ( MaxADSet (M /\ ( Cl A))) by Th5;

    theorem :: TSP_2:8

    for M be Subset of X st M is maximal_T_0 holds for A be Subset of X holds ( Int A) = ( MaxADSet (M /\ ( Int A))) by Th6;

    definition

      let X be non empty TopSpace;

      let M be Subset of X;

      :: original: maximal_T_0

      redefine

      :: TSP_2:def6

      attr M is maximal_T_0 means for x be Point of X holds ex a be Point of X st a in M & (M /\ ( MaxADSet x)) = {a};

      compatibility

      proof

        thus M is maximal_T_0 implies for x be Point of X holds ex a be Point of X st a in M & (M /\ ( MaxADSet x)) = {a}

        proof

          assume

           A1: M is maximal_T_0;

          then

           A2: M is T_0;

          let x be Point of X;

          x in ( MaxADSet M) by A1;

          then x in ( union { ( MaxADSet a) where a be Point of X : a in M }) by TEX_4:def 11;

          then

          consider C be set such that

           A3: x in C and

           A4: C in { ( MaxADSet a) where a be Point of X : a in M } by TARSKI:def 4;

          consider a be Point of X such that

           A5: C = ( MaxADSet a) and

           A6: a in M by A4;

          ( MaxADSet a) = ( MaxADSet x) by A3, A5, TEX_4: 21;

          then (M /\ ( MaxADSet x)) = {a} by A2, A6;

          hence thesis by A6;

        end;

        assume

         A7: for x be Point of X holds ex a be Point of X st a in M & (M /\ ( MaxADSet x)) = {a};

        now

          let x be object;



           A8: M c= ( MaxADSet M) by TEX_4: 32;

          assume x in the carrier of X;

          then

          reconsider y = x as Point of X;

          consider a be Point of X such that

           A9: a in M and

           A10: (M /\ ( MaxADSet y)) = {a} by A7;

           {a} c= ( MaxADSet y) by A10, XBOOLE_1: 17;

          then a in ( MaxADSet y) by ZFMISC_1: 31;

          then (( MaxADSet y) /\ ( MaxADSet M)) <> {} by A9, A8, XBOOLE_0:def 4;

          then ( MaxADSet y) meets ( MaxADSet M) by XBOOLE_0:def 7;

          then

           A11: ( MaxADSet y) c= ( MaxADSet M) by TEX_4: 30;

           {y} c= ( MaxADSet y) by TEX_4: 18;

          then y in ( MaxADSet y) by ZFMISC_1: 31;

          hence x in ( MaxADSet M) by A11;

        end;

        then the carrier of X c= ( MaxADSet M) by TARSKI:def 3;

        then

         A12: ( MaxADSet M) = the carrier of X by XBOOLE_0:def 10;

        for b be Point of X st b in M holds (M /\ ( MaxADSet b)) = {b}

        proof

          let b be Point of X;



           A13: ex a be Point of X st a in M & (M /\ ( MaxADSet b)) = {a} by A7;

           {b} c= ( MaxADSet b) by TEX_4: 18;

          then

           A14: b in ( MaxADSet b) by ZFMISC_1: 31;

          assume b in M;

          then b in (M /\ ( MaxADSet b)) by A14, XBOOLE_0:def 4;

          hence thesis by A13, TARSKI:def 1;

        end;

        then M is T_0;

        hence thesis by A12;

      end;

    end

    theorem :: TSP_2:9



     Th9: for A be Subset of X holds A is T_0 implies ex M be Subset of X st A c= M & M is maximal_T_0

    proof

      let A be Subset of X;

      set D = (( [#] X) \ ( MaxADSet A));

      set F = { ( MaxADSet d) where d be Point of X : d in D };

      now

        let C be object;

        assume C in F;

        then ex a be Point of X st C = ( MaxADSet a) & a in D;

        hence C in ( bool the carrier of X);

      end;

      then

      reconsider F as Subset-Family of X by TARSKI:def 3;

      assume

       A1: A is T_0;

      defpred X[ Subset of X, set] means $2 in D & $2 in $1;



       A2: D = (( MaxADSet A) ` );

      then

       A3: ( MaxADSet A) misses D by SUBSET_1: 24;

      A c= ( MaxADSet A) by TEX_4: 32;

      then A misses D by A2, SUBSET_1: 24;

      then

       A4: (A /\ D) = {} by XBOOLE_0:def 7;

      reconsider F as Subset-Family of X;



       A5: for S be Subset of X st S in F holds ex x be Point of X st X[S, x]

      proof

        let S be Subset of X;

        assume S in F;

        then

        consider d be Point of X such that

         A6: S = ( MaxADSet d) and

         A7: d in D;

        take d;

         {d} c= ( MaxADSet d) by TEX_4: 18;

        hence thesis by A6, A7, ZFMISC_1: 31;

      end;

      consider f be Function of F, the carrier of X such that

       A8: for S be Subset of X st S in F holds X[S, (f . S)] from TEX_2:sch 1( A5);

      set M = (A \/ (f .: F));

      now

        let x be object;

        assume x in (f .: F);

        then ex S be object st S in F & S in F & x = (f . S) by FUNCT_2: 64;

        hence x in D by A8;

      end;

      then (f .: F) c= D by TARSKI:def 3;

      then

       A9: ( MaxADSet A) misses (f .: F) by A3, XBOOLE_1: 63;

      thus ex M be Subset of X st A c= M & M is maximal_T_0

      proof

        take M;

        thus

         A10: A c= M by XBOOLE_1: 7;

        for x be Point of X holds ex a be Point of X st a in M & (M /\ ( MaxADSet x)) = {a}

        proof

          let x be Point of X;



           A11: ( [#] X) = (( MaxADSet A) \/ D) by XBOOLE_1: 45;

          now

            per cases by A11, XBOOLE_0:def 3;

              suppose

               A12: x in ( MaxADSet A);

              now

                 {x} c= ( MaxADSet A) by A12, ZFMISC_1: 31;

                then ( MaxADSet {x}) c= ( MaxADSet A) by TEX_4: 34;

                then ( MaxADSet x) c= ( MaxADSet A) by TEX_4: 28;

                then (f .: F) misses ( MaxADSet x) by A9, XBOOLE_1: 63;

                then ((f .: F) /\ ( MaxADSet x)) = {} by XBOOLE_0:def 7;

                then

                 A13: (M /\ ( MaxADSet x)) = ((A /\ ( MaxADSet x)) \/ {} ) by XBOOLE_1: 23;

                x in ( union { ( MaxADSet a) where a be Point of X : a in A }) by A12, TEX_4:def 11;

                then

                consider C be set such that

                 A14: x in C and

                 A15: C in { ( MaxADSet a) where a be Point of X : a in A } by TARSKI:def 4;

                consider a be Point of X such that

                 A16: C = ( MaxADSet a) and

                 A17: a in A by A15;

                take a;

                thus a in M by A10, A17;

                ( MaxADSet a) = ( MaxADSet x) by A14, A16, TEX_4: 21;

                hence (M /\ ( MaxADSet x)) = {a} by A1, A17, A13;

              end;

              hence thesis;

            end;

              suppose

               A18: x in D;

              then

               A19: ( MaxADSet x) in F;

              now

                reconsider a = (f . ( MaxADSet x)) as Point of X by A19, FUNCT_2: 5;

                take a;



                 A20: (f .: F) c= M by XBOOLE_1: 7;

                now

                  let y be object;

                  assume

                   A21: y in (M /\ ( MaxADSet x));

                  then

                  reconsider z = y as Point of X;



                   A22: z in M by A21, XBOOLE_0:def 4;



                   A23: z in ( MaxADSet x) by A21, XBOOLE_0:def 4;

                  then

                   A24: ( MaxADSet z) = ( MaxADSet x) by TEX_4: 21;

                  now

                    assume not ( MaxADSet x) c= D;

                    then ( MaxADSet x) meets ( MaxADSet A) by A2, SUBSET_1: 23;

                    then

                     A25: ( MaxADSet x) c= ( MaxADSet A) by TEX_4: 30;

                     {x} c= ( MaxADSet x) by TEX_4: 18;

                    then x in ( MaxADSet x) by ZFMISC_1: 31;

                    hence contradiction by A3, A18, A25, XBOOLE_0: 3;

                  end;

                  then not z in A by A4, A23, XBOOLE_0:def 4;

                  then z in (f .: F) by A22, XBOOLE_0:def 3;

                  then

                  consider C be object such that

                   A26: C in F and C in F and

                   A27: z = (f . C) by FUNCT_2: 64;

                  reconsider C as Subset of X by A26;

                  consider w be Point of X such that

                   A28: C = ( MaxADSet w) and w in D by A26;

                  z in ( MaxADSet w) by A8, A26, A27, A28;

                  then (f . ( MaxADSet w)) = a by A24, TEX_4: 21;

                  hence y in {a} by A27, A28, TARSKI:def 1;

                end;

                then

                 A29: (M /\ ( MaxADSet x)) c= {a} by TARSKI:def 3;



                 A30: a in (f .: F) by A19, FUNCT_2: 35;

                hence a in M by A20;

                a in ( MaxADSet x) by A8, A19;

                then

                 A31: {a} c= ( MaxADSet x) by ZFMISC_1: 31;

                 {a} c= M by A20, A30, ZFMISC_1: 31;

                then {a} c= (M /\ ( MaxADSet x)) by A31, XBOOLE_1: 19;

                hence (M /\ ( MaxADSet x)) = {a} by A29, XBOOLE_0:def 10;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence M is maximal_T_0;

      end;

    end;

    theorem :: TSP_2:10



     Th10: ex M be Subset of X st M is maximal_T_0

    proof

      set A = ( {} X);

      A is discrete by TEX_2: 29;

      then

      consider M be Subset of X such that A c= M and

       A1: M is maximal_T_0 by Th9, TSP_1: 9;

      take M;

      thus thesis by A1;

    end;

    begin

    definition

      let Y be non empty TopStruct;

      let IT be SubSpace of Y;

      :: TSP_2:def7

      attr IT is maximal_T_0 means for A be Subset of Y st A = the carrier of IT holds A is maximal_T_0;

    end

    theorem :: TSP_2:11



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

     Lm1:

    now

      let Z be non empty 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;

    registration

      let Y be non empty TopStruct;

      cluster maximal_T_0 -> T_0 for non empty SubSpace of Y;

      coherence

      proof

        let Y0 be non empty SubSpace of Y;

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

        assume Y0 is maximal_T_0;

        then A is maximal_T_0;

        then A is T_0;

        hence thesis by TSP_1: 13;

      end;

      cluster non T_0 -> non maximal_T_0 for non empty SubSpace of Y;

      coherence ;

    end

    definition

      let X be non empty TopSpace;

      let X0 be non empty SubSpace of X;

      :: original: maximal_T_0

      redefine

      :: TSP_2:def8

      attr X0 is maximal_T_0 means X0 is T_0 & for Y0 be T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0;

      compatibility

      proof

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        thus X0 is maximal_T_0 implies X0 is T_0 & for Y0 be T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0

        proof

          assume X0 is maximal_T_0;

          then

           A1: A is maximal_T_0;

          then A is T_0;

          hence X0 is T_0 by TSP_1: 13;

          thus for Y0 be T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0

          proof

            let Y0 be T_0 non empty SubSpace of X;

            reconsider D = the carrier of Y0 as Subset of X by TSEP_1: 1;

            assume X0 is SubSpace of Y0;

            then

             A2: A c= D by TSEP_1: 4;

            D is T_0 by TSP_1: 13;

            then A = D by A1, A2;

            hence thesis by TSEP_1: 5;

          end;

        end;

        assume X0 is T_0;

        then

         A3: A is T_0 by TSP_1: 13;

        assume

         A4: for Y0 be T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0;

        now

          let D be Subset of X;

          assume

           A5: D is T_0;

          assume

           A6: A c= D;

          then D <> {} ;

          then

          consider Y0 be T_0 strict non empty SubSpace of X such that

           A7: D = the carrier of Y0 by A5, TSP_1: 18;

          X0 is SubSpace of Y0 by A6, A7, TSEP_1: 4;

          hence A = D by A4, A7;

        end;

        then A is maximal_T_0 by A3;

        hence thesis;

      end;

    end

    reserve X for non empty TopSpace;

    theorem :: TSP_2:12



     Th12: for A0 be non empty Subset of X st A0 is maximal_T_0 holds ex X0 be strict non empty SubSpace of X st X0 is maximal_T_0 & A0 = the carrier of X0

    proof

      let A0 be non empty Subset of X;

      assume

       A1: A0 is maximal_T_0;

      consider X0 be strict non empty SubSpace of X such that

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

      take X0;

      thus thesis by A1, A2;

    end;

    registration

      let X be non empty TopSpace;

      cluster maximal_T_0 -> dense for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by Lm1;

        assume X0 is maximal_T_0;

        then A is maximal_T_0;

        then A is dense by Th2;

        hence thesis by TEX_3: 9;

      end;

      cluster non dense -> non maximal_T_0 for SubSpace of X;

      coherence ;

      cluster open maximal_T_0 -> non proper for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by Lm1;

        assume X0 is open;

        then

         A1: A is open by TSEP_1: 16;

        assume X0 is maximal_T_0;

        then A is maximal_T_0;

        then A is non proper by A1, Th3;

        hence thesis by TEX_2: 8;

      end;

      cluster open proper -> non maximal_T_0 for SubSpace of X;

      coherence ;

      cluster proper maximal_T_0 -> non open for SubSpace of X;

      coherence ;

      cluster closed maximal_T_0 -> non proper for SubSpace of X;

      coherence

      proof

        let X0 be SubSpace of X;

        reconsider A = the carrier of X0 as Subset of X by Lm1;

        assume X0 is closed;

        then

         A2: A is closed by TSEP_1: 11;

        assume X0 is maximal_T_0;

        then A is maximal_T_0;

        then A is non proper by A2, Th3;

        hence thesis by TEX_2: 8;

      end;

      cluster closed proper -> non maximal_T_0 for SubSpace of X;

      coherence ;

      cluster proper maximal_T_0 -> non closed for SubSpace of X;

      coherence ;

    end

    theorem :: TSP_2:13

    for Y0 be T_0 non empty SubSpace of X holds ex X0 be strict SubSpace of X st Y0 is SubSpace of X0 & X0 is maximal_T_0

    proof

      let Y0 be T_0 non empty SubSpace of X;

      reconsider A = the carrier of Y0 as Subset of X by Lm1;

      A is T_0 by TSP_1: 13;

      then

      consider M be Subset of X such that

       A1: A c= M and

       A2: M is maximal_T_0 by Th9;

      M is non empty by A2, Th4;

      then

      consider X0 be strict non empty SubSpace of X such that

       A3: X0 is maximal_T_0 and

       A4: M = the carrier of X0 by A2, Th12;

      take X0;

      thus thesis by A1, A3, A4, TSEP_1: 4;

    end;

    registration

      let X be non empty TopSpace;

      cluster maximal_T_0 strict non empty for SubSpace of X;

      existence

      proof

        consider M be Subset of X such that

         A1: M is maximal_T_0 by Th10;

        M is non empty by A1, Th4;

        then

        consider X0 be strict non empty SubSpace of X such that

         A2: X0 is maximal_T_0 and M = the carrier of X0 by A1, Th12;

        take X0;

        thus thesis by A2;

      end;

    end

    definition

      let X be non empty TopSpace;

      mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;

    end

    theorem :: TSP_2:14



     Th14: for X0 be maximal_Kolmogorov_subspace of X holds for G be Subset of X, G0 be Subset of X0 st G0 = G holds G0 is open iff ( MaxADSet G) is open & G0 = (( MaxADSet G) /\ the carrier of X0)

    proof

      let X0 be maximal_Kolmogorov_subspace of X;

      let G be Subset of X, G0 be Subset of X0;

      reconsider M = the carrier of X0 as Subset of X by Lm1;

      assume

       A1: G0 = G;



       A2: M is maximal_T_0 by Th11;

      thus G0 is open implies ( MaxADSet G) is open & G0 = (( MaxADSet G) /\ the carrier of X0)

      proof

        assume G0 is open;

        then

         A3: ex H be Subset of X st H is open & G0 = (H /\ M) by TSP_1:def 1;

        hence ( MaxADSet G) is open by A2, A1, Th6;

        thus thesis by A2, A1, A3, Th6;

      end;

      assume

       A4: ( MaxADSet G) is open;

      assume G0 = (( MaxADSet G) /\ the carrier of X0);

      hence thesis by A4, TSP_1:def 1;

    end;

    theorem :: TSP_2:15

    for X0 be maximal_Kolmogorov_subspace of X holds for G be Subset of X holds G is open iff G = ( MaxADSet G) & ex G0 be Subset of X0 st G0 is open & G0 = (G /\ the carrier of X0)

    proof

      let X0 be maximal_Kolmogorov_subspace of X;

      let G be Subset of X;

      reconsider M = the carrier of X0 as Subset of X by Lm1;

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

      proof

        reconsider G0 = (G /\ M) as Subset of X0 by XBOOLE_1: 17;

        reconsider G0 as Subset of X0;

        assume

         A1: G is open;

        hence G = ( MaxADSet G) by TEX_4: 56;

        take G0;

        thus G0 is open by A1, TSP_1:def 1;

        thus thesis;

      end;

      assume

       A2: G = ( MaxADSet G);

      given G0 be Subset of X0 such that

       A3: G0 is open and

       A4: G0 = (G /\ the carrier of X0);

      set E = G0;

      E c= M;

      then

      reconsider E as Subset of X by XBOOLE_1: 1;



       A5: E c= ( MaxADSet G) by A2, A4, XBOOLE_1: 17;



       A6: M is maximal_T_0 by Th11;

      for x be object st x in G holds x in ( MaxADSet E)

      proof

        let x be object;

        assume

         A7: x in G;

        then

        reconsider a = x as Point of X;

        consider b be Point of X such that

         A8: b in M and

         A9: (M /\ ( MaxADSet a)) = {b} by A6;



         A10: {b} c= ( MaxADSet a) by A9, XBOOLE_1: 17;

         {a} c= G by A7, ZFMISC_1: 31;

        then ( MaxADSet {a}) c= G by A2, TEX_4: 34;

        then ( MaxADSet a) c= G by TEX_4: 28;

        then {b} c= G by A10, XBOOLE_1: 1;

        then b in G by ZFMISC_1: 31;

        then b in E by A4, A8, XBOOLE_0:def 4;

        then {b} c= E by ZFMISC_1: 31;

        then ( MaxADSet {b}) c= ( MaxADSet E) by TEX_4: 31;

        then

         A11: ( MaxADSet b) c= ( MaxADSet E) by TEX_4: 28;

        b in ( MaxADSet a) by A10, ZFMISC_1: 31;

        then ( MaxADSet b) = ( MaxADSet a) by TEX_4: 21;

        then {a} c= ( MaxADSet b) by TEX_4: 18;

        then a in ( MaxADSet b) by ZFMISC_1: 31;

        hence thesis by A11;

      end;

      then

       A12: G c= ( MaxADSet E) by TARSKI:def 3;

      ( MaxADSet E) is open by A3, Th14;

      hence thesis by A2, A5, A12, TEX_4: 35;

    end;

    theorem :: TSP_2:16



     Th16: for X0 be maximal_Kolmogorov_subspace of X holds for F be Subset of X, F0 be Subset of X0 st F0 = F holds F0 is closed iff ( MaxADSet F) is closed & F0 = (( MaxADSet F) /\ the carrier of X0)

    proof

      let X0 be maximal_Kolmogorov_subspace of X;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      let F be Subset of X, F0 be Subset of X0;

      assume

       A1: F0 = F;



       A2: M is maximal_T_0 by Th11;

      thus F0 is closed implies ( MaxADSet F) is closed & F0 = (( MaxADSet F) /\ the carrier of X0)

      proof

        assume F0 is closed;

        then

         A3: ex H be Subset of X st H is closed & F0 = (H /\ M) by TSP_1:def 2;

        hence ( MaxADSet F) is closed by A2, A1, Th5;

        thus thesis by A2, A1, A3, Th5;

      end;

      assume

       A4: ( MaxADSet F) is closed;

      assume F0 = (( MaxADSet F) /\ the carrier of X0);

      hence thesis by A4, TSP_1:def 2;

    end;

    theorem :: TSP_2:17

    for X0 be maximal_Kolmogorov_subspace of X holds for F be Subset of X holds F is closed iff F = ( MaxADSet F) & ex F0 be Subset of X0 st F0 is closed & F0 = (F /\ the carrier of X0)

    proof

      let X0 be maximal_Kolmogorov_subspace of X;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      let F be Subset of X;

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

      proof

        set F0 = (F /\ M);

        reconsider F0 as Subset of X0 by XBOOLE_1: 17;

        assume

         A1: F is closed;

        hence F = ( MaxADSet F) by TEX_4: 60;

        take F0;

        thus F0 is closed by A1, TSP_1:def 2;

        thus thesis;

      end;

      assume

       A2: F = ( MaxADSet F);

      given F0 be Subset of X0 such that

       A3: F0 is closed and

       A4: F0 = (F /\ the carrier of X0);

      set E = F0;

      E c= M;

      then

      reconsider E as Subset of X by XBOOLE_1: 1;



       A5: E c= ( MaxADSet F) by A2, A4, XBOOLE_1: 17;



       A6: M is maximal_T_0 by Th11;

      for x be object st x in F holds x in ( MaxADSet E)

      proof

        let x be object;

        assume

         A7: x in F;

        then

        reconsider a = x as Point of X;

        consider b be Point of X such that

         A8: b in M and

         A9: (M /\ ( MaxADSet a)) = {b} by A6;



         A10: {b} c= ( MaxADSet a) by A9, XBOOLE_1: 17;

         {a} c= F by A7, ZFMISC_1: 31;

        then ( MaxADSet {a}) c= F by A2, TEX_4: 34;

        then ( MaxADSet a) c= F by TEX_4: 28;

        then {b} c= F by A10, XBOOLE_1: 1;

        then b in F by ZFMISC_1: 31;

        then b in E by A4, A8, XBOOLE_0:def 4;

        then {b} c= E by ZFMISC_1: 31;

        then ( MaxADSet {b}) c= ( MaxADSet E) by TEX_4: 31;

        then

         A11: ( MaxADSet b) c= ( MaxADSet E) by TEX_4: 28;

        b in ( MaxADSet a) by A10, ZFMISC_1: 31;

        then ( MaxADSet b) = ( MaxADSet a) by TEX_4: 21;

        then {a} c= ( MaxADSet b) by TEX_4: 18;

        then a in ( MaxADSet b) by ZFMISC_1: 31;

        hence thesis by A11;

      end;

      then

       A12: F c= ( MaxADSet E) by TARSKI:def 3;

      ( MaxADSet E) is closed by A3, Th16;

      hence thesis by A2, A5, A12, TEX_4: 35;

    end;

    begin

    reserve X for non empty TopSpace,

X0 for non empty maximal_Kolmogorov_subspace of X;

    theorem :: TSP_2:18



     Th18: for r be Function of X, X0 holds for M be Subset of X st M = the carrier of X0 holds (for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)}) implies r is continuous Function of X, X0

    proof

      let r be Function of X, X0;

      let M be Subset of X;

      assume

       A1: M = the carrier of X0;

      reconsider N = M as Subset of X;

      assume

       A2: for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)};



       A3: N is maximal_T_0 by A1, Th11;

      then

       A4: N is T_0;

      for F be Subset of X0 holds F is closed implies (r " F) is closed

      proof

        let F be Subset of X0;

        reconsider E = F as Subset of X by A1, XBOOLE_1: 1;

        set R = { ( MaxADSet a) where a be Point of X : a in E };

        now

          let x be object;

          assume

           A5: x in (r " F);

          then

          reconsider b = x as Point of X;



           A6: (r . b) in F by A5, FUNCT_2: 38;

          E c= the carrier of X;

          then

          reconsider a = (r . b) as Point of X by A6;

          ( MaxADSet a) in R by A6;

          then

           A7: ( MaxADSet a) c= ( union R) by ZFMISC_1: 74;

          (M /\ ( MaxADSet b)) = {a} by A2;

          then a in (M /\ ( MaxADSet b)) by ZFMISC_1: 31;

          then a in ( MaxADSet b) by XBOOLE_0:def 4;

          then

           A8: ( MaxADSet a) = ( MaxADSet b) by TEX_4: 21;



           A9: {b} c= ( MaxADSet b) by TEX_4: 18;

          b in {b} by TARSKI:def 1;

          then b in ( MaxADSet a) by A8, A9;

          hence x in ( union R) by A7;

        end;

        then

         A10: (r " F) c= ( union R) by TARSKI:def 3;

        assume F is closed;

        then ex P be Subset of X st P is closed & (P /\ ( [#] X0)) = F by PRE_TOPC: 13;

        then

         A11: ( MaxADSet E) is closed by A1, A3, Th5;

        now

          let C be set;

          assume C in R;

          then

          consider a be Point of X such that

           A12: C = ( MaxADSet a) and

           A13: a in E;

          now

            let x be object;

            assume

             A14: x in C;

            then

            reconsider b = x as Point of X by A12;



             A15: (M /\ ( MaxADSet b)) = {(r . b)} by A2;



             A16: (M /\ ( MaxADSet a)) = {a} by A1, A4, A13;

            ( MaxADSet a) = ( MaxADSet b) by A12, A14, TEX_4: 21;

            then a = (r . x) by A16, A15, ZFMISC_1: 3;

            hence x in (r " F) by A12, A13, A14, FUNCT_2: 38;

          end;

          hence C c= (r " F) by TARSKI:def 3;

        end;

        then

         A17: ( union R) c= (r " F) by ZFMISC_1: 76;

        ( union R) = ( MaxADSet E) by TEX_4:def 11;

        hence thesis by A11, A17, A10, XBOOLE_0:def 10;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;

    theorem :: TSP_2:19

    for r be Function of X, X0 holds (for a be Point of X holds (r . a) in ( MaxADSet a)) implies r is continuous Function of X, X0

    proof

      let r be Function of X, X0;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      assume

       A1: for a be Point of X holds (r . a) in ( MaxADSet a);

      M is maximal_T_0 by Th11;

      then

       A2: M is T_0;



       A3: M c= the carrier of X;

      for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)}

      proof

        let a be Point of X;

        reconsider s = (r . a) as Point of X by A3, TARSKI:def 3;



         A4: s in ( MaxADSet a) by A1;

        (M /\ ( MaxADSet s)) = {s} by A2;

        hence thesis by A4, TEX_4: 21;

      end;

      hence thesis by Th18;

    end;

    theorem :: TSP_2:20



     Th20: for r be continuous Function of X, X0 holds for M be Subset of X st M = the carrier of X0 holds (for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)}) implies r is being_a_retraction

    proof

      let r be continuous Function of X, X0;

      let M be Subset of X;

      reconsider N = M as Subset of X;

      assume

       A1: M = the carrier of X0;

      then N is maximal_T_0 by Th11;

      then

       A2: N is T_0;

      assume

       A3: for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)};

      for x be Point of X st x in the carrier of X0 holds (r . x) = x

      proof

        let x be Point of X;

        assume x in the carrier of X0;

        then

         A4: (M /\ ( MaxADSet x)) = {x} by A1, A2;

        (M /\ ( MaxADSet x)) = {(r . x)} by A3;

        hence thesis by A4, ZFMISC_1: 3;

      end;

      hence thesis by BORSUK_1:def 16;

    end;

    theorem :: TSP_2:21



     Th21: for r be continuous Function of X, X0 holds (for a be Point of X holds (r . a) in ( MaxADSet a)) implies r is being_a_retraction

    proof

      let r be continuous Function of X, X0;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      assume

       A1: for a be Point of X holds (r . a) in ( MaxADSet a);

      M is maximal_T_0 by Th11;

      then

       A2: M is T_0;



       A3: M c= the carrier of X;

      for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)}

      proof

        let a be Point of X;

        reconsider s = (r . a) as Point of X by A3, TARSKI:def 3;



         A4: s in ( MaxADSet a) by A1;

        (M /\ ( MaxADSet s)) = {s} by A2;

        hence thesis by A4, TEX_4: 21;

      end;

      hence thesis by Th20;

    end;

    theorem :: TSP_2:22



     Th22: ex r be continuous Function of X, X0 st r is being_a_retraction

    proof

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      defpred X[ Point of X, set] means (M /\ ( MaxADSet $1)) = {$2};



       A1: M is maximal_T_0 by Th11;



       A2: for x be Point of X holds ex a be Point of X0 st X[x, a]

      proof

        let x be Point of X;

        consider a be Point of X such that

         A3: a in M and

         A4: (M /\ ( MaxADSet x)) = {a} by A1;

        reconsider a as Point of X0 by A3;

        take a;

        thus thesis by A4;

      end;

      consider r be Function of X, X0 such that

       A5: for x be Point of X holds X[x, (r . x)] from FUNCT_2:sch 3( A2);

      reconsider r as continuous Function of X, X0 by A5, Th18;

      take r;

      thus thesis by A5, Th20;

    end;

    theorem :: TSP_2:23

    X0 is_a_retract_of X

    proof

      ex r be continuous Function of X, X0 st r is being_a_retraction by Th22;

      hence thesis by BORSUK_1:def 17;

    end;



     Lm2: for r be continuous Function of X, X0 holds r is being_a_retraction implies for a be Point of X, b be Point of X0 st a = b holds (r " ( Cl {b})) = ( Cl {a})

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      let a be Point of X, b be Point of X0;



       A2: b in {b} by TARSKI:def 1;

      assume

       A3: a = b;

      then (r . a) = b by A1, BORSUK_1:def 16;

      then

       A4: a in (r " {b}) by A2, FUNCT_2: 38;



       A5: A is maximal_T_0 by Th11;



       A6: (r " ( Cl {b})) c= ( Cl {a})

      proof

        assume not (r " ( Cl {b})) c= ( Cl {a});

        then

        consider c be object such that

         A7: c in (r " ( Cl {b})) and

         A8: not c in ( Cl {a}) by TARSKI:def 3;

        reconsider c as Point of X by A7;

        consider d be Point of X such that

         A9: d in A and

         A10: (A /\ ( MaxADSet c)) = {d} by A5;



         A11: {d} c= ( MaxADSet c) by A10, XBOOLE_1: 17;

        (r " ( Cl {b})) is closed by PRE_TOPC:def 6;

        then ( MaxADSet c) c= (r " ( Cl {b})) by A7, TEX_4: 23;

        then {d} c= (r " ( Cl {b})) by A11, XBOOLE_1: 1;

        then

         A12: d in (r " ( Cl {b})) by ZFMISC_1: 31;

        reconsider e = d as Point of X0 by A9;

         {c} c= ( MaxADSet c) by TEX_4: 18;

        then

         A13: c in ( MaxADSet c) by ZFMISC_1: 31;



         A14: ( Cl {b}) c= ( Cl {a}) by A3, TOPS_3: 53;

        (r . d) = e by A1, BORSUK_1:def 16;

        then e in ( Cl {b}) by A12, FUNCT_2: 38;

        then

         A15: ( MaxADSet d) c= ( Cl {a}) by A14, TEX_4: 23;

        d in ( MaxADSet c) by A11, ZFMISC_1: 31;

        then ( MaxADSet d) = ( MaxADSet c) by TEX_4: 21;

        hence contradiction by A8, A13, A15;

      end;



       A16: (r " ( Cl {b})) is closed by PRE_TOPC:def 6;

      (r " {b}) c= (r " ( Cl {b})) by PRE_TOPC: 18, RELAT_1: 143;

      then {a} c= (r " ( Cl {b})) by A4, ZFMISC_1: 31;

      then ( Cl {a}) c= (r " ( Cl {b})) by A16, TOPS_1: 5;

      hence thesis by A6, XBOOLE_0:def 10;

    end;



     Lm3: for r be continuous Function of X, X0 holds r is being_a_retraction implies for A be Subset of X st A = the carrier of X0 holds for a be Point of X holds (A /\ ( MaxADSet a)) = {(r . a)}

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

      let A be Subset of X;

      reconsider N = A as Subset of X;

      assume

       A2: A = the carrier of X0;

      let a be Point of X;



       A3: N is maximal_T_0 by A2, Th11;

      then

      consider c be Point of X such that

       A4: c in A and

       A5: (A /\ ( MaxADSet a)) = {c};



       A6: {c} c= ( MaxADSet c) by TEX_4: 18;

      (r . a) in A by A2;

      then

      reconsider d = (r . a) as Point of X;

       {(r . a)} c= ( Cl {(r . a)}) by PRE_TOPC: 18;

      then

       A7: (r . a) in ( Cl {(r . a)}) by ZFMISC_1: 31;

       {c} c= ( MaxADSet a) by A5, XBOOLE_1: 17;

      then c in ( MaxADSet a) by ZFMISC_1: 31;

      then

       A8: ( MaxADSet c) = ( MaxADSet a) by TEX_4: 21;

      reconsider b = c as Point of X0 by A2, A4;



       A9: {a} c= ( MaxADSet a) by TEX_4: 18;



       A10: (r " ( Cl {b})) = ( Cl {c}) by A1, Lm2;

      then {c} c= (r " ( Cl {b})) by PRE_TOPC: 18;

      then c in (r " ( Cl {b})) by ZFMISC_1: 31;

      then ( MaxADSet a) c= (r " ( Cl {b})) by A10, A8, TEX_4: 23;

      then {a} c= (r " ( Cl {b})) by A9, XBOOLE_1: 1;

      then a in (r " ( Cl {b})) by ZFMISC_1: 31;

      then

       A11: (r . a) in ( Cl {b}) by FUNCT_2: 38;

      (r " ( Cl {(r . a)})) = ( Cl {d}) by A1, Lm2;

      then a in ( Cl {d}) by A7, FUNCT_2: 38;

      then ( MaxADSet c) c= ( Cl {d}) by A8, TEX_4: 23;

      then {c} c= ( Cl {d}) by A6, XBOOLE_1: 1;

      then

       A12: ( Cl {c}) c= ( Cl {d}) by TOPS_1: 5;

      ( Cl {b}) c= ( Cl {c}) by TOPS_3: 53;

      then {d} c= ( Cl {c}) by A11, ZFMISC_1: 31;

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

      then ( Cl {d}) = ( Cl {c}) by A12, XBOOLE_0:def 10;

      then

       A13: ( MaxADSet d) = ( MaxADSet a) by A8, TEX_4: 49;

      N is T_0 by A3;

      hence thesis by A2, A13;

    end;



     Lm4: for r be continuous Function of X, X0 holds r is being_a_retraction implies for a be Point of X, b be Point of X0 st a = b holds ( MaxADSet a) c= (r " {b})

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      let a be Point of X, b be Point of X0;

      assume

       A2: a = b;

      assume not ( MaxADSet a) c= (r " {b});

      then

      consider s be object such that

       A3: s in ( MaxADSet a) and

       A4: not s in (r " {b}) by TARSKI:def 3;

      reconsider s as Point of X by A3;



       A5: ( MaxADSet a) = ( MaxADSet s) by A3, TEX_4: 21;



       A6: {s} c= ( MaxADSet s) by TEX_4: 18;



       A7: (r " ( Cl {b})) = ( Cl {a}) by A1, A2, Lm2;

      then {a} c= (r " ( Cl {b})) by PRE_TOPC: 18;

      then a in (r " ( Cl {b})) by ZFMISC_1: 31;

      then ( MaxADSet s) c= (r " ( Cl {b})) by A7, A5, TEX_4: 23;

      then {s} c= (r " ( Cl {b})) by A6, XBOOLE_1: 1;

      then s in (r " ( Cl {b})) by ZFMISC_1: 31;

      then

       A8: (r . s) in ( Cl {b}) by FUNCT_2: 38;

      A c= the carrier of X;

      then

      reconsider d = (r . s) as Point of X by TARSKI:def 3;

       {(r . s)} c= ( Cl {(r . s)}) by PRE_TOPC: 18;

      then

       A9: (r . s) in ( Cl {(r . s)}) by ZFMISC_1: 31;



       A10: {a} c= ( MaxADSet a) by TEX_4: 18;

      (r " ( Cl {(r . s)})) = ( Cl {d}) by A1, Lm2;

      then s in ( Cl {d}) by A9, FUNCT_2: 38;

      then ( MaxADSet a) c= ( Cl {d}) by A5, TEX_4: 23;

      then {a} c= ( Cl {d}) by A10, XBOOLE_1: 1;

      then

       A11: ( Cl {a}) c= ( Cl {d}) by TOPS_1: 5;

      ( Cl {b}) c= ( Cl {a}) by A2, TOPS_3: 53;

      then {d} c= ( Cl {a}) by A8, ZFMISC_1: 31;

      then ( Cl {d}) c= ( Cl {a}) by TOPS_1: 5;

      then ( Cl {d}) = ( Cl {a}) by A11, XBOOLE_0:def 10;

      then

       A12: ( MaxADSet d) = ( MaxADSet a) by TEX_4: 49;

      A is maximal_T_0 by Th11;

      then

       A13: A is T_0;

      (r . a) = b by A1, A2, BORSUK_1:def 16;

      then (A /\ ( MaxADSet a)) = {b} by A1, Lm3;

      then {b} = {(r . s)} by A13, A12;

      then (r . s) in {b} by ZFMISC_1: 31;

      hence contradiction by A4, FUNCT_2: 38;

    end;



     Lm5: for r be continuous Function of X, X0 holds r is being_a_retraction implies for a be Point of X, b be Point of X0 st a = b holds (r " {b}) = ( MaxADSet a)

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      let a be Point of X, b be Point of X0;

      assume

       A2: a = b;



       A3: (r " {b}) c= ( MaxADSet a)

      proof

        assume not (r " {b}) c= ( MaxADSet a);

        then

        consider s be object such that

         A4: s in (r " {b}) and

         A5: not s in ( MaxADSet a) by TARSKI:def 3;

        reconsider s as Point of X by A4;

        (r . s) in {b} by A4, FUNCT_2: 38;

        then {(r . s)} c= {b} by ZFMISC_1: 31;

        then {(r . s)} = {b} by ZFMISC_1: 18;

        then (A /\ ( MaxADSet s)) = {b} by A1, Lm3;

        then {a} c= ( MaxADSet s) by A2, XBOOLE_1: 17;

        then a in ( MaxADSet s) by ZFMISC_1: 31;

        then

         A6: ( MaxADSet s) = ( MaxADSet a) by TEX_4: 21;

         {s} c= ( MaxADSet s) by TEX_4: 18;

        hence contradiction by A5, A6, ZFMISC_1: 31;

      end;

      ( MaxADSet a) c= (r " {b}) by A1, A2, Lm4;

      hence thesis by A3, XBOOLE_0:def 10;

    end;



     Lm6: for r be continuous Function of X, X0 holds r is being_a_retraction implies for E be Subset of X, F be Subset of X0 st F = E holds (r " F) = ( MaxADSet E)

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      let E be Subset of X, F be Subset of X0;

      set R = { ( MaxADSet a) where a be Point of X : a in E };

      assume

       A2: F = E;

      now

        let x be object;

        assume

         A3: x in (r " F);

        then

        reconsider b = x as Point of X;



         A4: (r . b) in F by A3, FUNCT_2: 38;

        then

        reconsider a = (r . b) as Point of X by A2;

        ( MaxADSet a) in R by A2, A4;

        then

         A5: ( MaxADSet a) c= ( union R) by ZFMISC_1: 74;

        (A /\ ( MaxADSet b)) = {a} by A1, Lm3;

        then a in (A /\ ( MaxADSet b)) by ZFMISC_1: 31;

        then a in ( MaxADSet b) by XBOOLE_0:def 4;

        then

         A6: ( MaxADSet a) = ( MaxADSet b) by TEX_4: 21;

         {b} c= ( MaxADSet b) by TEX_4: 18;

        then b in ( MaxADSet a) by A6, ZFMISC_1: 31;

        hence x in ( union R) by A5;

      end;

      then

       A7: (r " F) c= ( union R) by TARSKI:def 3;

      A is maximal_T_0 by Th11;

      then

       A8: A is T_0;

      now

        let C be set;

        assume C in R;

        then

        consider a be Point of X such that

         A9: C = ( MaxADSet a) and

         A10: a in E;

        now

          let x be object;

          assume

           A11: x in C;

          then

          reconsider b = x as Point of X by A9;



           A12: (A /\ ( MaxADSet b)) = {(r . b)} by A1, Lm3;



           A13: (A /\ ( MaxADSet a)) = {a} by A2, A8, A10;

          ( MaxADSet a) = ( MaxADSet b) by A9, A11, TEX_4: 21;

          then a = (r . x) by A13, A12, ZFMISC_1: 3;

          hence x in (r " F) by A2, A9, A10, A11, FUNCT_2: 38;

        end;

        hence C c= (r " F) by TARSKI:def 3;

      end;

      then

       A14: ( union R) c= (r " F) by ZFMISC_1: 76;

      ( MaxADSet E) = ( union R) by TEX_4:def 11;

      hence thesis by A14, A7, XBOOLE_0:def 10;

    end;

    definition

      let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X;

      :: TSP_2:def9

      func Stone-retraction (X,X0) -> continuous Function of X, X0 means

      : Def9: it is being_a_retraction;

      existence by Th22;

      uniqueness

      proof

        reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1: 1;

        let r1,r2 be continuous Function of X, X0;

        assume that

         A1: r1 is being_a_retraction and

         A2: r2 is being_a_retraction;

        for x be object st x in the carrier of X holds (r1 . x) = (r2 . x)

        proof

          let x be object;

          assume x in the carrier of X;

          then

          reconsider a = x as Point of X;



           A3: (M /\ ( MaxADSet a)) = {(r2 . a)} by A2, Lm3;

          (M /\ ( MaxADSet a)) = {(r1 . a)} by A1, Lm3;

          hence thesis by A3, ZFMISC_1: 3;

        end;

        hence r1 = r2 by FUNCT_2: 12;

      end;

    end

    theorem :: TSP_2:24

    for a be Point of X, b be Point of X0 st a = b holds (( Stone-retraction (X,X0)) " ( Cl {b})) = ( Cl {a}) by Def9, Lm2;

    theorem :: TSP_2:25



     Th25: for a be Point of X, b be Point of X0 st a = b holds (( Stone-retraction (X,X0)) " {b}) = ( MaxADSet a) by Def9, Lm5;

    theorem :: TSP_2:26



     Th26: for E be Subset of X, F be Subset of X0 st F = E holds (( Stone-retraction (X,X0)) " F) = ( MaxADSet E) by Def9, Lm6;

    definition

      let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X;

      :: original: Stone-retraction

      redefine

      :: TSP_2:def10

      func Stone-retraction (X,X0) means

      : Def10: for M be Subset of X st M = the carrier of X0 holds for a be Point of X holds (M /\ ( MaxADSet a)) = {(it . a)};

      compatibility

      proof

        reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

        let r be continuous Function of X, X0;

        thus r = ( Stone-retraction (X,X0)) implies for M be Subset of X st M = the carrier of X0 holds for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)} by Def9, Lm3;

        assume for A be Subset of X st A = the carrier of X0 holds for a be Point of X holds (A /\ ( MaxADSet a)) = {(r . a)};

        then for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)};

        then r is being_a_retraction by Th20;

        hence r = ( Stone-retraction (X,X0)) by Def9;

      end;

    end

    definition

      let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X;

      :: original: Stone-retraction

      redefine

      :: TSP_2:def11

      func Stone-retraction (X,X0) means

      : Def11: for a be Point of X holds (it . a) in ( MaxADSet a);

      compatibility

      proof

        reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

        let r be continuous Function of X, X0;

        thus r = ( Stone-retraction (X,X0)) implies for a be Point of X holds (r . a) in ( MaxADSet a)

        proof

          assume

           A1: r = ( Stone-retraction (X,X0));

          let a be Point of X;

          (A /\ ( MaxADSet a)) = {(r . a)} by A1, Def10;

          then {(r . a)} c= ( MaxADSet a) by XBOOLE_1: 17;

          hence thesis by ZFMISC_1: 31;

        end;

        assume for a be Point of X holds (r . a) in ( MaxADSet a);

        then r is being_a_retraction by Th21;

        hence r = ( Stone-retraction (X,X0)) by Def9;

      end;

    end

    theorem :: TSP_2:27



     Th27: for a be Point of X holds (( Stone-retraction (X,X0)) " {(( Stone-retraction (X,X0)) . a)}) = ( MaxADSet a)

    proof

      let a be Point of X;

      reconsider A = the carrier of X0 as Subset of X by TSEP_1: 1;

      set r = ( Stone-retraction (X,X0));

      (r . a) in A;

      then

      reconsider b = (r . a) as Point of X;



       A1: (r . a) in ( MaxADSet a) by Def11;

      (r " {(r . a)}) = ( MaxADSet b) by Th25;

      hence thesis by A1, TEX_4: 21;

    end;

    theorem :: TSP_2:28

    for a be Point of X holds ( Im (( Stone-retraction (X,X0)),a)) = (( Stone-retraction (X,X0)) .: ( MaxADSet a))

    proof

      let a be Point of X;

      set r = ( Stone-retraction (X,X0));



       A1: ( dom r) = ( [#] X) by FUNCT_2:def 1;



       A2: (r .: (r " {(r . a)})) c= {(r . a)} by FUNCT_1: 75;



       A3: (r " {(r . a)}) = ( MaxADSet a) by Th27;

      then (r .: (r " {(r . a)})) <> {} by A1, RELAT_1: 119;

      then (r .: (r " {(r . a)})) = {(r . a)} by A2, ZFMISC_1: 33;

      hence thesis by A1, A3, FUNCT_1: 59;

    end;

    definition

      let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X;

      :: original: Stone-retraction

      redefine

      :: TSP_2:def12

      func Stone-retraction (X,X0) means

      : Def12: for M be Subset of X st M = the carrier of X0 holds for A be Subset of X holds (M /\ ( MaxADSet A)) = (it .: A);

      compatibility

      proof

        let r be continuous Function of X, X0;

        thus r = ( Stone-retraction (X,X0)) implies for M be Subset of X st M = the carrier of X0 holds for A be Subset of X holds (M /\ ( MaxADSet A)) = (r .: A)

        proof

          assume

           A1: r = ( Stone-retraction (X,X0));

          let M be Subset of X;

          reconsider N = M as Subset of X;

          assume

           A2: M = the carrier of X0;

          let A be Subset of X;

          N is maximal_T_0 by A2, Th11;

          then

           A3: N is T_0;

          for x be object st x in (M /\ ( MaxADSet A)) holds x in (r .: A)

          proof

            let x be object;

            assume

             A4: x in (M /\ ( MaxADSet A));

            then

            reconsider c = x as Point of X;

            c in M by A4, XBOOLE_0:def 4;

            then

             A5: (M /\ ( MaxADSet c)) = {c} by A3;

            c in ( MaxADSet A) by A4, XBOOLE_0:def 4;

            then c in ( union { ( MaxADSet a) where a be Point of X : a in A }) by TEX_4:def 11;

            then

            consider D be set such that

             A6: c in D and

             A7: D in { ( MaxADSet a) where a be Point of X : a in A } by TARSKI:def 4;

            consider a be Point of X such that

             A8: D = ( MaxADSet a) and

             A9: a in A by A7;

            ( MaxADSet c) = ( MaxADSet a) by A6, A8, TEX_4: 21;

            then {(r . a)} = {c} by A1, A2, A5, Def10;

            hence thesis by A9, FUNCT_2: 35, ZFMISC_1: 3;

          end;

          then

           A10: (M /\ ( MaxADSet A)) c= (r .: A) by TARSKI:def 3;

          for x be object st x in (r .: A) holds x in (M /\ ( MaxADSet A))

          proof

            let x be object;

            assume

             A11: x in (r .: A);

            then

            reconsider b = x as Point of X0;

            consider a be object such that

             A12: a in the carrier of X and

             A13: a in A and

             A14: b = (r . a) by A11, FUNCT_2: 64;

            reconsider a as Point of X by A12;

             {a} c= A by A13, ZFMISC_1: 31;

            then ( MaxADSet {a}) c= ( MaxADSet A) by TEX_4: 31;

            then ( MaxADSet a) c= ( MaxADSet A) by TEX_4: 28;

            then

             A15: (M /\ ( MaxADSet a)) c= (M /\ ( MaxADSet A)) by XBOOLE_1: 26;

            (M /\ ( MaxADSet a)) = {b} by A1, A2, A14, Def10;

            hence thesis by A15, ZFMISC_1: 31;

          end;

          then (r .: A) c= (M /\ ( MaxADSet A)) by TARSKI:def 3;

          hence thesis by A10, XBOOLE_0:def 10;

        end;

        assume

         A16: for M be Subset of X st M = the carrier of X0 holds for A be Subset of X holds (M /\ ( MaxADSet A)) = (r .: A);



         A17: ( dom r) = ( [#] X) by FUNCT_2:def 1;

        for M be Subset of X st M = the carrier of X0 holds for a be Point of X holds (M /\ ( MaxADSet a)) = {(r . a)}

        proof

          let M be Subset of X;

          assume

           A18: M = the carrier of X0;

          let a be Point of X;

          (M /\ ( MaxADSet {a})) = ( Im (r,a)) by A16, A18;

          then (M /\ ( MaxADSet a)) = ( Im (r,a)) by TEX_4: 28;

          hence thesis by A17, FUNCT_1: 59;

        end;

        hence r = ( Stone-retraction (X,X0)) by Def10;

      end;

    end

    theorem :: TSP_2:29



     Th29: for A be Subset of X holds (( Stone-retraction (X,X0)) " (( Stone-retraction (X,X0)) .: A)) = ( MaxADSet A)

    proof

      let A be Subset of X;

      reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1: 1;

      set r = ( Stone-retraction (X,X0));

      C c= the carrier of X;

      then

      reconsider B = (r .: A) as Subset of X by XBOOLE_1: 1;

      (C /\ ( MaxADSet A)) = B by Def12;

      then

       A1: B c= ( MaxADSet A) by XBOOLE_1: 17;



       A2: (r " (r .: A)) = ( MaxADSet B) by Th26;

      then A c= ( MaxADSet B) by FUNCT_2: 42;

      hence thesis by A2, A1, TEX_4: 35;

    end;

    theorem :: TSP_2:30

    for A be Subset of X holds (( Stone-retraction (X,X0)) .: A) = (( Stone-retraction (X,X0)) .: ( MaxADSet A))

    proof

      let A be Subset of X;

      set r = ( Stone-retraction (X,X0));



       A1: ( rng r) = (r .: the carrier of X) by RELSET_1: 22;

      (r .: (r " (r .: A))) = (r .: ( MaxADSet A)) by Th29;

      hence thesis by A1, FUNCT_1: 77, RELAT_1: 123;

    end;

    theorem :: TSP_2:31

    for A,B be Subset of X holds (( Stone-retraction (X,X0)) .: (A \/ B)) = ((( Stone-retraction (X,X0)) .: A) \/ (( Stone-retraction (X,X0)) .: B))

    proof

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      set r = ( Stone-retraction (X,X0));

      let A,B be Subset of X;

      (r .: (A \/ B)) = (M /\ ( MaxADSet (A \/ B))) by Def12

      .= (M /\ (( MaxADSet A) \/ ( MaxADSet B))) by TEX_4: 36

      .= ((M /\ ( MaxADSet A)) \/ (M /\ ( MaxADSet B))) by XBOOLE_1: 23

      .= ((r .: A) \/ (M /\ ( MaxADSet B))) by Def12

      .= ((r .: A) \/ (r .: B)) by Def12;

      hence thesis;

    end;

    theorem :: TSP_2:32

    for A,B be Subset of X st A is open or B is open holds (( Stone-retraction (X,X0)) .: (A /\ B)) = ((( Stone-retraction (X,X0)) .: A) /\ (( Stone-retraction (X,X0)) .: B))

    proof

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      set r = ( Stone-retraction (X,X0));

      let A,B be Subset of X;

      assume

       A1: A is open or B is open;

      (r .: (A /\ B)) = (M /\ ( MaxADSet (A /\ B))) by Def12

      .= ((M /\ M) /\ (( MaxADSet A) /\ ( MaxADSet B))) by A1, TEX_4: 65

      .= (M /\ (M /\ (( MaxADSet A) /\ ( MaxADSet B)))) by XBOOLE_1: 16

      .= (((M /\ ( MaxADSet A)) /\ ( MaxADSet B)) /\ M) by XBOOLE_1: 16

      .= ((M /\ ( MaxADSet A)) /\ (M /\ ( MaxADSet B))) by XBOOLE_1: 16

      .= ((r .: A) /\ (M /\ ( MaxADSet B))) by Def12

      .= ((r .: A) /\ (r .: B)) by Def12;

      hence thesis;

    end;

    theorem :: TSP_2:33

    for A,B be Subset of X st A is closed or B is closed holds (( Stone-retraction (X,X0)) .: (A /\ B)) = ((( Stone-retraction (X,X0)) .: A) /\ (( Stone-retraction (X,X0)) .: B))

    proof

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      set r = ( Stone-retraction (X,X0));

      let A,B be Subset of X;

      assume

       A1: A is closed or B is closed;

      (r .: (A /\ B)) = (M /\ ( MaxADSet (A /\ B))) by Def12

      .= ((M /\ M) /\ (( MaxADSet A) /\ ( MaxADSet B))) by A1, TEX_4: 64

      .= (M /\ (M /\ (( MaxADSet A) /\ ( MaxADSet B)))) by XBOOLE_1: 16

      .= (((M /\ ( MaxADSet A)) /\ ( MaxADSet B)) /\ M) by XBOOLE_1: 16

      .= ((M /\ ( MaxADSet A)) /\ (M /\ ( MaxADSet B))) by XBOOLE_1: 16

      .= ((r .: A) /\ (M /\ ( MaxADSet B))) by Def12

      .= ((r .: A) /\ (r .: B)) by Def12;

      hence thesis;

    end;

    theorem :: TSP_2:34

    for A be Subset of X holds A is open implies (( Stone-retraction (X,X0)) .: A) is open

    proof

      let A be Subset of X;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      set B = (( Stone-retraction (X,X0)) .: A);

      assume

       A1: A is open;

      then A = ( MaxADSet A) by TEX_4: 56;

      then (A /\ M) = B by Def12;

      hence thesis by A1, TSP_1:def 1;

    end;

    theorem :: TSP_2:35

    for A be Subset of X holds A is closed implies (( Stone-retraction (X,X0)) .: A) is closed

    proof

      let A be Subset of X;

      reconsider M = the carrier of X0 as Subset of X by TSEP_1: 1;

      set B = (( Stone-retraction (X,X0)) .: A);

      assume

       A1: A is closed;

      then A = ( MaxADSet A) by TEX_4: 60;

      then (A /\ M) = B by Def12;

      hence thesis by A1, TSP_1:def 2;

    end;