tex_2.miz



    begin

    theorem :: TEX_2:1

    

     Th1: for A be non empty set, B be 1 -element set st A c= B holds A = B

    proof

      let A be non empty set, B be 1 -element set;

      assume

       A1: A c= B;

      ex s be Element of B st B = {s} by SUBSET_1: 46;

      hence thesis by A1, ZFMISC_1: 33;

    end;

    theorem :: TEX_2:2

    for A be 1 -element set, B be set st (A /\ B) is non empty holds A c= B

    proof

      let A be 1 -element set, B be set;

      

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

      assume (A /\ B) is non empty;

      then

      consider a be object such that

       A2: a in (A /\ B);

      

       A3: ex s be Element of A st A = {s} by SUBSET_1: 46;

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

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

      then {a} = A by A3, ZFMISC_1: 18;

      hence thesis by A2, A1, ZFMISC_1: 31;

    end;

    registration

      let S be 1 -element set;

      cluster proper -> empty for Subset of S;

      coherence

      proof

        let A be Subset of S;

        assume A is proper;

        then

         A1: A <> S;

        ex s be Element of S st S = {s} by SUBSET_1: 46;

        hence thesis by A1, ZFMISC_1: 33;

      end;

      cluster non empty -> non proper for Subset of S;

      coherence ;

    end

    theorem :: TEX_2:3

    for S be non empty set, y be Element of S holds {y} is proper implies S is non trivial;

    theorem :: TEX_2:4

    for S be non trivial set, y be Element of S holds {y} is proper;

    registration

      let S be 1 -element set;

      cluster non proper -> trivial for non empty Subset of S;

      coherence ;

    end

    registration

      let S be non trivial set;

      cluster trivial -> proper for non empty Subset of S;

      coherence ;

      cluster non proper -> non trivial for non empty Subset of S;

      coherence ;

    end

    registration

      let S be non trivial set;

      cluster trivial proper for non empty Subset of S;

      existence

      proof

        set A = the trivial non empty Subset of S;

        take A;

        thus thesis;

      end;

      cluster non trivial non proper for non empty Subset of S;

      existence

      proof

        take ( [#] S);

        thus thesis;

      end;

    end

    theorem :: TEX_2:5

    for Y be non empty 1-sorted, y be Element of Y holds {y} is proper implies Y is non trivial;

    theorem :: TEX_2:6

    for Y be non trivial 1-sorted, y be Element of Y holds {y} is proper;

    registration

      let Y be 1 -element 1-sorted;

      cluster -> non proper for non empty Subset of Y;

      coherence ;

      cluster non proper -> trivial for non empty Subset of Y;

      coherence ;

    end

    registration

      let Y be non trivial 1-sorted;

      cluster trivial -> proper for non empty Subset of Y;

      coherence ;

      cluster non proper -> non trivial for non empty Subset of Y;

      coherence ;

    end

    registration

      let Y be non trivial 1-sorted;

      cluster trivial proper for non empty Subset of Y;

      existence

      proof

        set A = the trivial non empty Subset of Y;

        take A;

        thus thesis;

      end;

      cluster non trivial non proper for non empty Subset of Y;

      existence

      proof

        take ( [#] Y);

        thus thesis;

      end;

    end

    registration

      let Y be non trivial 1-sorted;

      cluster non empty trivial proper for Subset of Y;

      existence

      proof

        set X = the trivial proper non empty Subset of Y;

        reconsider X as Subset of Y;

        take X;

        thus thesis;

      end;

    end

    registration

      let X be non empty set;

      let A be proper Subset of X;

      cluster (A ` ) -> non empty;

      coherence

      proof

        assume (A ` ) is empty;

        then ((A ` ) ` ) = X;

        hence thesis by SUBSET_1:def 6;

      end;

    end

    begin

    theorem :: TEX_2:7

    for Y0,Y1 be TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is TopSpace-like implies Y1 is TopSpace-like;

    definition

      let Y be TopStruct;

      let IT be SubSpace of Y;

      :: TEX_2:def1

      attr IT is proper means

      : Def1: for A be Subset of Y st A = the carrier of IT holds A is proper;

    end

    reserve Y for TopStruct;

    theorem :: TEX_2:8

    for Y0 be SubSpace of Y, A be Subset of Y st A = the carrier of Y0 holds A is proper iff Y0 is proper;

     Lm1:

    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;

    theorem :: TEX_2:9

    for Y0,Y1 be SubSpace of Y st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is proper implies Y1 is proper;

    theorem :: TEX_2:10

    for Y0 be SubSpace of Y holds the carrier of Y0 = the carrier of Y implies Y0 is non proper

    proof

      let Y0 be SubSpace of Y;

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

      assume

       A1: the carrier of Y0 = the carrier of Y;

      now

        take A;

        thus A = the carrier of Y0 & A is non proper by A1;

      end;

      hence thesis;

    end;

    registration

      let Y be 1 -element TopStruct;

      cluster -> non proper for non empty SubSpace of Y;

      coherence

      proof

        let Y0 be non empty SubSpace of Y;

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

        now

          take A;

          thus A = the carrier of Y0 & A is non proper;

        end;

        hence thesis;

      end;

      cluster non proper -> trivial for non empty SubSpace of Y;

      coherence ;

    end

    registration

      let Y be non trivial TopStruct;

      cluster trivial -> proper for non empty SubSpace of Y;

      coherence ;

      cluster non proper -> non trivial for non empty SubSpace of Y;

      coherence ;

    end

    registration

      let Y be non empty TopStruct;

      cluster non proper strict non empty for SubSpace of Y;

      existence

      proof

        ( [#] Y) = the carrier of Y;

        then

        reconsider A0 = the carrier of Y as non empty Subset of Y;

        set Y0 = (Y | A0);

        take Y0;

        A0 = ( [#] Y0) by PRE_TOPC:def 5;

        hence thesis;

      end;

    end

    theorem :: TEX_2:11

    for Y be non empty TopStruct, Y0 be non proper SubSpace of Y holds the TopStruct of Y0 = the TopStruct of Y

    proof

      let Y be non empty TopStruct;

      let Y0 be non proper SubSpace of Y;

      

       A1: ex A be Subset of Y st A = the carrier of Y0 & A is non proper by Def1;

      now

        let D be object;

        assume

         A2: D in the topology of Y;

        then

        reconsider E = D as Subset of Y;

        reconsider C = E as Subset of Y0 by A1;

        now

          take E;

          thus E in the topology of Y & C = (E /\ ( [#] Y0)) by A2, XBOOLE_1: 28;

        end;

        hence D in the topology of Y0 by PRE_TOPC:def 4;

      end;

      then

       A3: the topology of Y c= the topology of Y0 by TARSKI:def 3;

      

       A4: the carrier of Y0 = the carrier of Y by A1;

      now

        let D be object;

        assume

         A5: D in the topology of Y0;

        then

        reconsider C = D as Subset of Y0;

        ex E be Subset of Y st E in the topology of Y & C = (E /\ ( [#] Y0)) by A5, PRE_TOPC:def 4;

        hence D in the topology of Y by A4, XBOOLE_1: 28;

      end;

      then the topology of Y0 c= the topology of Y by TARSKI:def 3;

      then the topology of Y0 = the topology of Y by A3;

      hence thesis by A1;

    end;

    registration

      let Y be non empty TopStruct;

      cluster discrete -> TopSpace-like for SubSpace of Y;

      coherence ;

      cluster anti-discrete -> TopSpace-like for SubSpace of Y;

      coherence ;

      cluster non TopSpace-like -> non discrete for SubSpace of Y;

      coherence ;

      cluster non TopSpace-like -> non anti-discrete for SubSpace of Y;

      coherence ;

    end

    theorem :: TEX_2:12

    

     Th12: for Y0,Y1 be TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is discrete implies Y1 is discrete

    proof

      let Y0,Y1 be TopStruct;

      assume

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

      assume Y0 is discrete;

      then the topology of Y0 = ( bool the carrier of Y0) by TDLAT_3:def 1;

      hence thesis by A1, TDLAT_3:def 1;

    end;

    theorem :: TEX_2:13

    for Y0,Y1 be TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is anti-discrete implies Y1 is anti-discrete

    proof

      let Y0,Y1 be TopStruct;

      assume

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

      assume Y0 is anti-discrete;

      then the topology of Y0 = { {} , the carrier of Y0} by TDLAT_3:def 2;

      hence thesis by A1, TDLAT_3:def 2;

    end;

    registration

      let Y be non empty TopStruct;

      cluster discrete -> almost_discrete for SubSpace of Y;

      coherence ;

      cluster non almost_discrete -> non discrete for SubSpace of Y;

      coherence ;

      cluster anti-discrete -> almost_discrete for SubSpace of Y;

      coherence ;

      cluster non almost_discrete -> non anti-discrete for SubSpace of Y;

      coherence ;

    end

    theorem :: TEX_2:14

    for Y0,Y1 be TopStruct st the TopStruct of Y0 = the TopStruct of Y1 holds Y0 is almost_discrete implies Y1 is almost_discrete

    proof

      let Y0,Y1 be TopStruct;

      assume

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

      assume Y0 is almost_discrete;

      then for A be Subset of Y0 st A in the topology of Y0 holds (the carrier of Y0 \ A) in the topology of Y0 by TDLAT_3:def 3;

      hence thesis by A1, TDLAT_3:def 3;

    end;

    registration

      let Y be non empty TopStruct;

      cluster discrete anti-discrete -> trivial for non empty SubSpace of Y;

      coherence ;

      cluster anti-discrete non trivial -> non discrete for non empty SubSpace of Y;

      coherence ;

      cluster discrete non trivial -> non anti-discrete for non empty SubSpace of Y;

      coherence ;

    end

    definition

      let Y be non empty TopStruct, y be Point of Y;

      :: TEX_2:def2

      func Sspace (y) -> strict non empty SubSpace of Y means

      : Def2: the carrier of it = {y};

      existence

      proof

        reconsider D = {y} as non empty Subset of Y;

        set Y0 = (Y | D);

        take Y0;

        D = ( [#] Y0) by PRE_TOPC:def 5;

        hence thesis;

      end;

      uniqueness

      proof

        let Y1,Y2 be strict non empty SubSpace of Y;

        assume that

         A1: the carrier of Y1 = {y} and

         A2: the carrier of Y2 = {y};

        set A1 = the carrier of Y1, A2 = the carrier of Y2;

        

         A3: A2 = ( [#] Y2);

        

         A4: A1 = ( [#] Y1);

        then A1 c= ( [#] Y) by PRE_TOPC:def 4;

        then

        reconsider A1 as Subset of Y;

        Y1 = (Y | A1) by A4, PRE_TOPC:def 5;

        hence thesis by A1, A2, A3, PRE_TOPC:def 5;

      end;

    end

     Lm2:

    now

      let Y be non empty TopStruct, y be Point of Y;

      set Y0 = ( Sspace y);

      the carrier of Y0 = {y} by Def2;

      then

      reconsider y0 = y as Point of Y0 by TARSKI:def 1;

      the carrier of Y0 = {y0} by Def2;

      hence ( Sspace y) is 1 -element;

    end;

    registration

      let Y be non empty TopStruct;

      cluster strict1 -element for SubSpace of Y;

      existence

      proof

        set y = the Point of Y;

        take ( Sspace y);

        thus thesis by Lm2;

      end;

    end

    registration

      let Y be non empty TopStruct, y be Point of Y;

      cluster ( Sspace y) -> 1 -element;

      coherence by Lm2;

    end

    theorem :: TEX_2:15

    for Y be non empty TopStruct, y be Point of Y holds ( Sspace y) is proper iff {y} is proper

    proof

      let Y be non empty TopStruct, y be Point of Y;

      hereby

        reconsider A = the carrier of ( Sspace y) as Subset of Y by Lm1;

        assume

         A1: ( Sspace y) is proper;

        A = {y} by Def2;

        hence {y} is proper by A1;

      end;

      thus thesis by Def2;

    end;

    theorem :: TEX_2:16

    for Y be non empty TopStruct, y be Point of Y holds ( Sspace y) is proper implies Y is non trivial;

    registration

      let Y be non trivial TopStruct;

      cluster proper trivial strict for non empty SubSpace of Y;

      existence

      proof

        take the trivial strict non empty SubSpace of Y;

        thus thesis;

      end;

    end

    registration

      let Y be non empty TopStruct;

      cluster 1 -element for SubSpace of Y;

      existence

      proof

        take Y0 = the trivial non empty SubSpace of Y;

        thus thesis;

      end;

    end

    theorem :: TEX_2:17

    for Y be non empty TopStruct, Y0 be 1 -element SubSpace of Y holds ex y be Point of Y st the TopStruct of Y0 = the TopStruct of ( Sspace y)

    proof

      let Y be non empty TopStruct, Y0 be 1 -element SubSpace of Y;

      consider y0 be Element of Y0 such that

       A1: the carrier of Y0 = {y0} by TEX_1:def 1;

      the carrier of Y0 is Subset of Y by Lm1;

      then

      reconsider y = y0 as Point of Y by A1, ZFMISC_1: 31;

      take y;

      the carrier of Y0 = the carrier of ( Sspace y) by A1, Def2;

      hence thesis by TSEP_1: 5;

    end;

    theorem :: TEX_2:18

    for Y be non empty TopStruct, y be Point of Y holds ( Sspace y) is TopSpace-like implies ( Sspace y) is discrete anti-discrete;

    registration

      let Y be non empty TopStruct;

      cluster trivial TopSpace-like -> discrete anti-discrete for non empty SubSpace of Y;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster trivial strict TopSpace-like non empty for SubSpace of X;

      existence

      proof

        set x = the Point of X;

        take ( Sspace x);

        thus thesis;

      end;

    end

    registration

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

      cluster ( Sspace x) -> TopSpace-like;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster discrete anti-discrete strict non empty for SubSpace of X;

      existence

      proof

        set x = the Point of X;

        take ( Sspace x);

        thus thesis;

      end;

    end

    registration

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

      cluster ( Sspace x) -> discrete anti-discrete;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

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

      coherence

      proof

        let X0 be SubSpace of X;

        assume X0 is non proper;

        then

         A1: ex A be Subset of X st A = the carrier of X0 & A is non proper;

        then

         A2: for A be Subset of X st A = the carrier of X0 holds A is closed;

        now

          let A be Subset of X;

          assume A = the carrier of X0;

          then A = ( [#] X) by A1;

          hence A is open;

        end;

        hence thesis by A2, BORSUK_1:def 11, TSEP_1:def 1;

      end;

      cluster non open -> proper for SubSpace of X;

      coherence ;

      cluster non closed -> proper for SubSpace of X;

      coherence ;

    end

    registration

      let X be non empty TopSpace;

      cluster open closed strict for SubSpace of X;

      existence

      proof

        set X0 = the non proper strict SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be discrete non empty TopSpace;

      cluster anti-discrete -> trivial for non empty SubSpace of X;

      coherence ;

      cluster non trivial -> non anti-discrete for non empty SubSpace of X;

      coherence ;

    end

    registration

      let X be discrete non trivial TopSpace;

      cluster discrete open closed proper strict for SubSpace of X;

      existence

      proof

        set X0 = the proper strict SubSpace of X;

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be anti-discrete non empty TopSpace;

      cluster discrete -> trivial for non empty SubSpace of X;

      coherence ;

      cluster non trivial -> non discrete for non empty SubSpace of X;

      coherence ;

    end

    registration

      let X be anti-discrete non trivial TopSpace;

      cluster -> non open non closed for proper non empty SubSpace of X;

      coherence

      proof

        let X0 be proper non empty SubSpace of X;

        assume

         A1: X0 is open or X0 is closed;

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

        set B = (A ` );

        

         A2: B <> the carrier of X by TOPS_3: 1;

        

         A3: A is proper by Def1;

        then

         A4: A <> the carrier of X;

        now

          per cases by A1;

            suppose X0 is open;

            then A is open by TSEP_1:def 1;

            then A in the topology of X;

            then A in { {} , the carrier of X} by TDLAT_3:def 2;

            hence contradiction by A4, TARSKI:def 2;

          end;

            suppose X0 is closed;

            then A is closed by BORSUK_1:def 11;

            then B in the topology of X by PRE_TOPC:def 2;

            then B in { {} , the carrier of X} by TDLAT_3:def 2;

            hence contradiction by A3, A2, TARSKI:def 2;

          end;

        end;

        hence thesis;

      end;

      cluster -> trivial proper for discrete non empty SubSpace of X;

      coherence ;

    end

    registration

      let X be anti-discrete non trivial TopSpace;

      cluster anti-discrete non open non closed proper strict for SubSpace of X;

      existence

      proof

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

        take X0;

        thus thesis;

      end;

    end

    registration

      let X be almost_discrete non trivial TopSpace;

      cluster almost_discrete proper strict non empty for SubSpace of X;

      existence

      proof

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

        take X0;

        thus thesis;

      end;

    end

    begin

    definition

      let Y be TopStruct, IT be Subset of Y;

      :: TEX_2:def3

      attr IT is discrete means for D be Subset of Y st D c= IT holds ex G be Subset of Y st G is open & (IT /\ G) = D;

    end

    definition

      let Y be TopStruct;

      let A be Subset of Y;

      :: original: discrete

      redefine

      :: TEX_2:def4

      attr A is discrete means for D be Subset of Y st D c= A holds ex F be Subset of Y st F is closed & (A /\ F) = D;

      compatibility

      proof

        hereby

          assume

           A1: A is discrete;

          let D be Subset of Y;

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

          then

          consider G be Subset of Y such that

           A2: G is open and

           A3: (A /\ G) = (A \ D) by A1;

          assume

           A4: D c= A;

          now

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

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

            hence F is closed by A2;

            (A /\ ( [#] Y)) = A by XBOOLE_1: 28;

            then (A /\ F) = (A \ G) by XBOOLE_1: 49;

            then (A /\ F) = (A \ (A \ D)) by A3, XBOOLE_1: 47;

            then (A /\ F) = (A /\ D) by XBOOLE_1: 48;

            hence (A /\ F) = D by A4, XBOOLE_1: 28;

          end;

          hence ex F be Subset of Y st F is closed & (A /\ F) = D;

        end;

        hereby

          assume

           A5: for D be Subset of Y st D c= A holds ex F be Subset of Y st F is closed & (A /\ F) = D;

          now

            let D be Subset of Y;

            consider F be Subset of Y such that

             A6: F is closed and

             A7: (A /\ F) = (A \ D) by A5, XBOOLE_1: 36;

            assume

             A8: D c= A;

            now

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

              thus G is open by A6;

              (A /\ ( [#] Y)) = A by XBOOLE_1: 28;

              then (A /\ G) = (A \ F) by XBOOLE_1: 49;

              then (A /\ G) = (A \ (A \ D)) by A7, XBOOLE_1: 47;

              then (A /\ G) = (A /\ D) by XBOOLE_1: 48;

              hence (A /\ G) = D by A8, XBOOLE_1: 28;

            end;

            hence ex G be Subset of Y st G is open & (A /\ G) = D;

          end;

          hence A is discrete;

        end;

      end;

    end

    theorem :: TEX_2:19

    

     Th19: 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 discrete implies D1 is discrete

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

      now

        let D be Subset of Y1;

        reconsider E = D as Subset of Y0 by A1;

        assume D c= D1;

        then

        consider G0 be Subset of Y0 such that

         A4: G0 is open and

         A5: (D0 /\ G0) = E by A2, A3;

        reconsider G = G0 as Subset of Y1 by A1;

        now

          take G;

          G in the topology of Y1 by A1, A4;

          hence G is open;

          thus (D1 /\ G) = D by A2, A5;

        end;

        hence ex G be Subset of Y1 st G is open & (D1 /\ G) = D;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:20

    

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

    proof

      let Y be non empty TopStruct, Y0 be non empty SubSpace of Y, A be Subset of Y;

      assume

       A1: A = the carrier of Y0;

      

       A2: ( [#] Y) = the carrier of Y;

      ( [#] Y0) = the carrier of Y0;

      then

       A3: the carrier of Y0 c= the carrier of Y by A2, PRE_TOPC:def 4;

      hereby

        assume

         A4: A is discrete;

        now

          let C be object;

          assume C in ( bool the carrier of Y0);

          then

          reconsider B = C as Subset of Y0;

          reconsider D = B as Subset of Y by A3, XBOOLE_1: 1;

          consider G be Subset of Y such that

           A5: G is open and

           A6: (A /\ G) = D by A1, A4;

          G in the topology of Y & B = (G /\ ( [#] Y0)) by A1, A6, A5;

          hence C in the topology of Y0 by PRE_TOPC:def 4;

        end;

        then ( bool the carrier of Y0) c= the topology of Y0 by TARSKI:def 3;

        then the topology of Y0 = ( bool the carrier of Y0);

        hence Y0 is discrete by TDLAT_3:def 1;

      end;

      hereby

        assume

         A7: Y0 is discrete;

        now

          let D be Subset of Y;

          assume D c= A;

          then

          reconsider B = D as Subset of Y0 by A1;

          B is open by A7, TDLAT_3: 15;

          then B in the topology of Y0;

          then

          consider G be Subset of Y such that

           A8: G in the topology of Y and

           A9: B = (G /\ ( [#] Y0)) by PRE_TOPC:def 4;

          reconsider G as Subset of Y;

          take G;

          thus G is open by A8;

          thus (A /\ G) = D by A1, A9;

        end;

        hence A is discrete;

      end;

    end;

    theorem :: TEX_2:21

    

     Th21: for Y be non empty TopStruct, A be Subset of Y st A = the carrier of Y holds A is discrete iff Y is discrete

    proof

      let Y be non empty TopStruct, A be Subset of Y;

      assume

       A1: A = the carrier of Y;

      hereby

        assume

         A2: A is discrete;

        now

          let C be object;

          assume C in ( bool the carrier of Y);

          then

          reconsider B = C as Subset of Y;

          consider G be Subset of Y such that

           A3: G is open and

           A4: (A /\ G) = B by A1, A2;

          G = B by A1, A4, XBOOLE_1: 28;

          hence C in the topology of Y by A3;

        end;

        then ( bool the carrier of Y) c= the topology of Y by TARSKI:def 3;

        then the topology of Y = ( bool the carrier of Y);

        hence Y is discrete by TDLAT_3:def 1;

      end;

      hereby

        assume Y is discrete;

        then

        reconsider Y as discrete non empty TopStruct;

        now

          let D be Subset of Y;

          assume

           A5: D c= A;

          reconsider G = D as Subset of Y;

          take G;

          thus G is open by TDLAT_3: 15;

          thus (A /\ G) = D by A5, XBOOLE_1: 28;

        end;

        hence A is discrete;

      end;

    end;

    theorem :: TEX_2:22

    

     Th22: for A,B be Subset of Y st B c= A holds A is discrete implies B is discrete

    proof

      let A,B be Subset of Y;

      assume

       A1: B c= A;

      assume

       A2: A is discrete;

      now

        let D be Subset of Y;

        assume

         A3: D c= B;

        then D c= A by A1, XBOOLE_1: 1;

        then

        consider G be Subset of Y such that

         A4: G is open and

         A5: (A /\ G) = D by A2;

        hereby

          take G;

          D c= G by A5, XBOOLE_1: 17;

          then

           A6: D c= (B /\ G) by A3, XBOOLE_1: 19;

          (B /\ G) c= (A /\ G) by A1, XBOOLE_1: 26;

          hence G is open & (B /\ G) = D by A4, A5, A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:23

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

    proof

      let A,B be Subset of Y;

      assume

       A1: A is discrete or B is discrete;

      hereby

        per cases by A1;

          suppose A is discrete;

          hence thesis by Th22, XBOOLE_1: 17;

        end;

          suppose B is discrete;

          hence thesis by Th22, XBOOLE_1: 17;

        end;

      end;

    end;

    theorem :: TEX_2:24

    

     Th24: (for P,Q be Subset of Y st P is open & Q is open holds (P /\ Q) is open & (P \/ Q) is open) implies for A,B be Subset of Y st A is open & B is open holds A is discrete & B is discrete implies (A \/ B) is discrete

    proof

      assume

       A1: for P,Q be Subset of Y st P is open & Q is open holds (P /\ Q) is open & (P \/ Q) is open;

      let A,B be Subset of Y;

      assume that

       A2: A is open and

       A3: B is open;

      assume that

       A4: A is discrete and

       A5: B is discrete;

      now

        let D be Subset of Y;

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

        then

        consider G1 be Subset of Y such that

         A6: G1 is open and

         A7: (A /\ G1) = (D /\ A) by A4;

        (D /\ B) c= B by XBOOLE_1: 17;

        then

        consider G2 be Subset of Y such that

         A8: G2 is open and

         A9: (B /\ G2) = (D /\ B) by A5;

        assume D c= (A \/ B);

        then

         A10: D = (D /\ (A \/ B)) by XBOOLE_1: 28;

        now

          take G = ((A /\ G1) \/ (B /\ G2));

          

           A11: (B /\ G2) is open by A1, A3, A8;

          (A /\ G1) is open by A1, A2, A6;

          hence G is open by A1, A11;

          thus ((A \/ B) /\ G) = D by A10, A7, A9, XBOOLE_1: 23;

        end;

        hence ex G be Subset of Y st G is open & ((A \/ B) /\ G) = D;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:25

    

     Th25: (for P,Q be Subset of Y st P is closed & Q is closed holds (P /\ Q) is closed & (P \/ Q) is closed) implies for A,B be Subset of Y st A is closed & B is closed holds A is discrete & B is discrete implies (A \/ B) is discrete

    proof

      assume

       A1: for P,Q be Subset of Y st P is closed & Q is closed holds (P /\ Q) is closed & (P \/ Q) is closed;

      let A,B be Subset of Y;

      assume that

       A2: A is closed and

       A3: B is closed;

      assume that

       A4: A is discrete and

       A5: B is discrete;

      now

        let D be Subset of Y;

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

        then

        consider F1 be Subset of Y such that

         A6: F1 is closed and

         A7: (A /\ F1) = (D /\ A) by A4;

        (D /\ B) c= B by XBOOLE_1: 17;

        then

        consider F2 be Subset of Y such that

         A8: F2 is closed and

         A9: (B /\ F2) = (D /\ B) by A5;

        assume D c= (A \/ B);

        then

         A10: D = (D /\ (A \/ B)) by XBOOLE_1: 28;

        now

          take F = ((A /\ F1) \/ (B /\ F2));

          

           A11: (B /\ F2) is closed by A1, A3, A8;

          (A /\ F1) is closed by A1, A2, A6;

          hence F is closed by A1, A11;

          thus ((A \/ B) /\ F) = D by A10, A7, A9, XBOOLE_1: 23;

        end;

        hence ex F be Subset of Y st F is closed & ((A \/ B) /\ F) = D;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:26

    

     Th26: for A be Subset of Y holds A is discrete implies for x be Point of Y st x in A holds ex G be Subset of Y st G is open & (A /\ G) = {x}

    proof

      let A be Subset of Y;

      assume

       A1: A is discrete;

      let x be Point of Y;

      assume

       A2: x in A;

      then

      reconsider Y9 = Y as non empty TopStruct;

      reconsider B = {x} as Subset of Y9 by ZFMISC_1: 31;

      reconsider A9 = A as Subset of Y9;

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

      then

      consider G be Subset of Y9 such that

       A3: G is open and

       A4: (A9 /\ G) = B by A1;

      reconsider G as Subset of Y;

      take G;

      thus thesis by A3, A4;

    end;

    theorem :: TEX_2:27

    for A be Subset of Y holds A is discrete implies for x be Point of Y st x in A holds ex F be Subset of Y st F is closed & (A /\ F) = {x}

    proof

      let A be Subset of Y;

      assume

       A1: A is discrete;

      let x be Point of Y;

      assume

       A2: x in A;

      then

      reconsider Y9 = Y as non empty TopStruct;

      reconsider B = {x} as Subset of Y9 by ZFMISC_1: 31;

      reconsider A9 = A as Subset of Y9;

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

      then

      consider F be Subset of Y such that

       A3: F is closed and

       A4: (A9 /\ F) = B by A1;

      take F;

      thus thesis by A3, A4;

    end;

    reserve X for non empty TopSpace;

    theorem :: TEX_2:28

    

     Th28: for A0 be non empty Subset of X st A0 is discrete holds ex X0 be discrete strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let 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 discrete;

      then

      reconsider X0 as discrete strict non empty SubSpace of X by A1, Th20;

      take X0;

      thus thesis by A1;

    end;

    theorem :: TEX_2:29

    

     Th29: for A be empty Subset of X holds A is discrete

    proof

      let A be empty Subset of X;

      now

        let D be Subset of X;

        assume

         A1: D c= A;

        now

          take G = ( {} X);

          thus G is open & (A /\ G) = D by A1;

        end;

        hence ex G be Subset of X st G is open & (A /\ G) = D;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:30

    

     Th30: for x be Point of X holds {x} is discrete

    proof

      let x be Point of X;

      now

        let D be Subset of X;

         A1:

        now

          assume

           A2: D = {} ;

          hereby

            take G = ( {} X);

            thus G is open & ( {x} /\ G) = D by A2;

          end;

        end;

         A3:

        now

          assume

           A4: D = {x};

          hereby

            take G = ( [#] X);

            thus G is open & ( {x} /\ G) = D by A4, XBOOLE_1: 28;

          end;

        end;

        assume D c= {x};

        hence ex G be Subset of X st G is open & ( {x} /\ G) = D by A1, A3, ZFMISC_1: 33;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:31

    

     Th31: for A be Subset of X holds (for x be Point of X st x in A holds ex G be Subset of X st G is open & (A /\ G) = {x}) implies A is discrete

    proof

      let A be Subset of X;

      assume

       A1: for x be Point of X st x in A holds ex G be Subset of X st G is open & (A /\ G) = {x};

      hereby

        per cases ;

          suppose A is empty;

          hence thesis by Th29;

        end;

          suppose A is non empty;

          then

          consider X0 be strict non empty SubSpace of X such that

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

          

           A3: ( [#] X) = the carrier of X;

          ( [#] X0) = the carrier of X0;

          then

           A4: the carrier of X0 c= the carrier of X by A3, PRE_TOPC:def 4;

          now

            let C be Subset of X0;

            let y be Point of X0;

            reconsider x = y as Point of X by A4, TARSKI:def 3;

            consider G be Subset of X such that

             A5: G is open and

             A6: (A /\ G) = {x} by A1, A2;

            assume

             A7: C = {y};

            G in the topology of X & (G /\ ( [#] X0)) = C by A2, A7, A6, A5;

            then C in the topology of X0 by PRE_TOPC:def 4;

            hence C is open;

          end;

          then X0 is discrete by TDLAT_3: 17;

          hence thesis by A2, Th20;

        end;

      end;

    end;

    theorem :: TEX_2:32

    for A,B be Subset of X st A is open & B is open holds A is discrete & B is discrete implies (A \/ B) is discrete

    proof

      let A,B be Subset of X;

      assume that

       A1: A is open and

       A2: B is open;

      assume that

       A3: A is discrete and

       A4: B is discrete;

      for P,Q be Subset of X st P is open & Q is open holds (P /\ Q) is open & (P \/ Q) is open;

      hence thesis by A1, A2, A3, A4, Th24;

    end;

    theorem :: TEX_2:33

    for A,B be Subset of X st A is closed & B is closed holds A is discrete & B is discrete implies (A \/ B) is discrete

    proof

      let A,B be Subset of X;

      assume that

       A1: A is closed and

       A2: B is closed;

      assume that

       A3: A is discrete and

       A4: B is discrete;

      for P,Q be Subset of X st P is closed & Q is closed holds (P /\ Q) is closed & (P \/ Q) is closed;

      hence thesis by A1, A2, A3, A4, Th25;

    end;

    

     Lm3: for P,Q be set st P c= Q & P <> Q holds (Q \ P) <> {}

    proof

      let P,Q be set;

      assume P c= Q;

      then

       A1: Q = (P \/ (Q \ P)) by XBOOLE_1: 45;

      assume

       A2: P <> Q;

      assume (Q \ P) = {} ;

      hence contradiction by A1, A2;

    end;

    theorem :: TEX_2:34

    for A be Subset of X st A is everywhere_dense holds A is discrete implies A is open

    proof

      let A be Subset of X;

      assume A is everywhere_dense;

      then

       A1: ( Cl ( Int A)) = the carrier of X by TOPS_3:def 5;

      assume

       A2: A is discrete;

      assume not A is open;

      then (A \ ( Int A)) <> {} by Lm3, TOPS_1: 16;

      then

      consider a be object such that

       A3: a in (A \ ( Int A)) by XBOOLE_0:def 1;

      reconsider a as Point of X by A3;

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

      then

      consider G be Subset of X such that

       A4: G is open and

       A5: (A /\ G) = {a} by A2, A3, Th26;

       A6:

      now

        assume (( Int A) /\ G) = {a};

        then {a} c= ( Int A) by XBOOLE_1: 17;

        then a in ( Int A) by ZFMISC_1: 31;

        hence contradiction by A3, XBOOLE_0:def 5;

      end;

      (( Int A) /\ G) c= {a} by A5, TOPS_1: 16, XBOOLE_1: 26;

      then (( Int A) /\ G) = {} or (( Int A) /\ G) = {a} by ZFMISC_1: 33;

      then ( Int A) misses G or (( Int A) /\ G) = {a};

      then ( Cl ( Int A)) misses G by A4, A6, TSEP_1: 36;

      then

       A7: (( Cl ( Int A)) /\ G) = {} ;

       {a} c= G by A5, XBOOLE_1: 17;

      hence contradiction by A1, A7, XBOOLE_1: 3, XBOOLE_1: 19;

    end;

    theorem :: TEX_2:35

    

     Th35: for A be Subset of X holds A is discrete iff for D be Subset of X st D c= A holds (A /\ ( Cl D)) = D

    proof

      let A be Subset of X;

      thus A is discrete implies for D be Subset of X st D c= A holds (A /\ ( Cl D)) = D

      proof

        assume

         A1: A is discrete;

        let D be Subset of X;

        assume

         A2: D c= A;

        then

        consider F be Subset of X such that

         A3: F is closed and

         A4: (A /\ F) = D by A1;

        ( Cl D) c= F by A3, A4, TOPS_1: 5, XBOOLE_1: 17;

        then

         A5: (A /\ ( Cl D)) c= D by A4, XBOOLE_1: 26;

        D c= ( Cl D) by PRE_TOPC: 18;

        then D c= (A /\ ( Cl D)) by A2, XBOOLE_1: 19;

        hence thesis by A5;

      end;

      assume

       A6: for D be Subset of X st D c= A holds (A /\ ( Cl D)) = D;

      now

        let D be Subset of X;

        assume

         A7: D c= A;

        now

          take F = ( Cl D);

          thus F is closed;

          thus (A /\ F) = D by A6, A7;

        end;

        hence ex F be Subset of X st F is closed & (A /\ F) = D;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:36

    

     Th36: for A be Subset of X holds A is discrete implies for x be Point of X st x in A holds (A /\ ( Cl {x})) = {x} by ZFMISC_1: 31, Th35;

    theorem :: TEX_2:37

    for X be discrete non empty TopSpace, A be Subset of X holds A is discrete

    proof

      let X be discrete non empty TopSpace, A be Subset of X;

      hereby

        per cases ;

          suppose A is empty;

          hence thesis by Th29;

        end;

          suppose A is non empty;

          then ex X0 be strict non empty SubSpace of X st A = the carrier of X0 by TSEP_1: 10;

          hence thesis by Th20;

        end;

      end;

    end;

    theorem :: TEX_2:38

    

     Th38: for X be anti-discrete non empty TopSpace, A be non empty Subset of X holds A is discrete iff A is trivial

    proof

      let X be anti-discrete non empty TopSpace, A be non empty Subset of X;

      hereby

        consider a be object such that

         A1: a in A by XBOOLE_0:def 1;

        reconsider a as Point of X by A1;

        assume A is discrete;

        then

        consider G be Subset of X such that

         A2: G is open and

         A3: (A /\ G) = {a} by A1, Th26;

        G <> {} by A3;

        then

         A4: G = the carrier of X by A2, TDLAT_3: 18;

        now

          take a;

          thus A = {a} by A3, A4, XBOOLE_1: 28;

        end;

        hence A is trivial;

      end;

      hereby

        assume A is trivial;

        then ex a be Element of A st A = {a} by SUBSET_1: 46;

        hence A is discrete by Th30;

      end;

    end;

    definition

      let Y be TopStruct, IT be Subset of Y;

      :: TEX_2:def5

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

    end

    theorem :: TEX_2:39

    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_discrete implies D1 is maximal_discrete

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

       A4:

      now

        let D be Subset of Y1;

        reconsider E = D as Subset of Y0 by A1;

        assume D is discrete;

        then

         A5: E is discrete by A1, Th19;

        assume D1 c= D;

        hence D1 = D by A2, A3, A5;

      end;

      D0 is discrete by A3;

      then D1 is discrete by A1, A2, Th19;

      hence thesis by A4;

    end;

    theorem :: TEX_2:40

    

     Th40: for A be empty Subset of X holds not A is maximal_discrete

    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 discrete & A c= C & A <> C by Th30, XBOOLE_1: 2;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:41

    

     Th41: for A be Subset of X st A is open holds A is maximal_discrete implies A is dense

    proof

      let A be Subset of X;

      assume

       A1: A is open;

      assume

       A2: A is maximal_discrete;

      then

       A3: A is discrete;

      assume not A is dense;

      then ( Cl A) <> the carrier of X by TOPS_3:def 2;

      then (the carrier of X \ ( Cl A)) <> {} by Lm3;

      then

      consider a be object such that

       A4: a in (the carrier of X \ ( Cl A)) by XBOOLE_0:def 1;

      reconsider a as Point of X by A4;

      set B = (A \/ {a});

      

       A5: A c= B by XBOOLE_1: 7;

       A6:

      now

        let x be Point of X;

        assume x in B;

        then

         A7: x in A or x in {a} by XBOOLE_0:def 3;

        now

          per cases by A7, TARSKI:def 1;

            suppose

             A8: x in A;

            then

             A9: ex G be Subset of X st G is open & (A /\ G) = {x} by A3, Th26;

            now

              take E = {x};

              thus E is open by A1, A9;

               {x} c= B by A5, A8, ZFMISC_1: 31;

              hence (B /\ E) = {x} by XBOOLE_1: 28;

            end;

            hence ex E be Subset of X st E is open & (B /\ E) = {x};

          end;

            suppose

             A10: x = a;

            now

              take G = (( [#] X) \ ( Cl A));

              

               A11: (B /\ G) = ((A /\ G) \/ ( {a} /\ G)) by XBOOLE_1: 23;

              

               A12: G = (( Cl A) ` );

              hence G is open;

              A c= ( Cl A) by PRE_TOPC: 18;

              then A misses G by A12, SUBSET_1: 24;

              then

               A13: (A /\ G) = {} ;

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

              hence (B /\ G) = {x} by A10, A13, A11, XBOOLE_1: 28;

            end;

            hence ex G be Subset of X st G is open & (B /\ G) = {x};

          end;

        end;

        hence ex G be Subset of X st G is open & (B /\ G) = {x};

      end;

      A c= ( Cl A) by PRE_TOPC: 18;

      then

       A14: not a in A by A4, XBOOLE_0:def 5;

      ex D be Subset of X st D is discrete & A c= D & A <> D

      proof

        take B;

        thus B is discrete by A6, Th31;

        thus A c= B by XBOOLE_1: 7;

        A <> B by A14, ZFMISC_1: 31, XBOOLE_1: 7;

        hence thesis;

      end;

      hence contradiction by A2;

    end;

    theorem :: TEX_2:42

    for A be Subset of X st A is dense holds A is discrete implies A is maximal_discrete

    proof

      let A be Subset of X;

      assume

       A1: A is dense;

      assume

       A2: A is discrete;

      assume not A is maximal_discrete;

      then

      consider D be Subset of X such that

       A3: D is discrete and

       A4: A c= D and

       A5: A <> D by A2;

      (D \ A) <> {} by A4, A5, Lm3;

      then

      consider a be object such that

       A6: a in (D \ A) by XBOOLE_0:def 1;

      reconsider a as Point of X by A6;

      a in D by A6, XBOOLE_0:def 5;

      then

      consider G be Subset of X such that

       A7: G is open and

       A8: (D /\ G) = {a} by A3, Th26;

       A9:

      now

        assume (A /\ G) = {a};

        then {a} c= A by XBOOLE_1: 17;

        then a in A by ZFMISC_1: 31;

        hence contradiction by A6, XBOOLE_0:def 5;

      end;

      (A /\ G) c= (D /\ G) by A4, XBOOLE_1: 26;

      then (A /\ G) = {} or (A /\ G) = {a} by A8, ZFMISC_1: 33;

      then A misses G or (A /\ G) = {a};

      then ( Cl A) misses G by A7, A9, TSEP_1: 36;

      then

       A10: (( Cl A) /\ G) = {} ;

      now

        assume ( Cl A) = the carrier of X;

        then G = {} by A10, XBOOLE_1: 28;

        hence contradiction by A8;

      end;

      hence contradiction by A1, TOPS_3:def 2;

    end;

    theorem :: TEX_2:43

    

     Th43: for X be discrete non empty TopSpace, A be Subset of X holds A is maximal_discrete iff A is non proper

    proof

      let X be discrete non empty TopSpace, A be Subset of X;

      hereby

        X is SubSpace of X by TSEP_1: 2;

        then

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

        assume

         A1: A is maximal_discrete;

        C is discrete by Th21;

        then A = C by A1;

        hence A is non proper;

      end;

      thus thesis by Th21, XBOOLE_0:def 10;

    end;

    theorem :: TEX_2:44

    

     Th44: for X be anti-discrete non empty TopSpace, A be non empty Subset of X holds A is maximal_discrete iff A is trivial

    proof

      let X be anti-discrete non empty TopSpace, A be non empty Subset of X;

      thus A is maximal_discrete implies A is trivial by Th38;

      hereby

         A1:

        now

          let D be Subset of X;

          assume

           A2: D is discrete;

          assume

           A3: A c= D;

          then

          reconsider E = D as non empty Subset of X;

          E is trivial by A2, Th38;

          hence A = D by A3, Th1;

        end;

        assume A is trivial;

        then A is discrete by Th38;

        hence A is maximal_discrete by A1;

      end;

    end;

    definition

      let Y be non empty TopStruct;

      let IT be SubSpace of Y;

      :: TEX_2:def6

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

    end

    theorem :: TEX_2:45

    

     Th45: 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_discrete iff Y0 is maximal_discrete;

    registration

      let Y be non empty TopStruct;

      cluster maximal_discrete -> discrete 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_discrete;

        then A is maximal_discrete;

        then A is discrete;

        hence thesis by Th20;

      end;

      cluster non discrete -> non maximal_discrete for non empty SubSpace of Y;

      coherence ;

    end

    theorem :: TEX_2:46

    for X0 be non empty SubSpace of X holds X0 is maximal_discrete iff X0 is discrete & for Y0 be discrete non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0

    proof

      let X0 be non empty SubSpace of X;

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

      hereby

        assume X0 is maximal_discrete;

        then

         A1: A is maximal_discrete;

        then A is discrete;

        hence X0 is discrete by Th20;

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

        proof

          let Y0 be discrete 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 discrete by Th20;

          then A = D by A1, A2;

          hence thesis by TSEP_1: 5;

        end;

      end;

      hereby

        assume X0 is discrete;

        then

         A3: A is discrete by Th20;

        assume

         A4: for Y0 be discrete 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 discrete;

          assume

           A6: A c= D;

          then D <> {} ;

          then

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

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

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

          hence A = D by A4, A7;

        end;

        then A is maximal_discrete by A3;

        hence X0 is maximal_discrete;

      end;

    end;

    theorem :: TEX_2:47

    

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

    proof

      let A0 be non empty Subset of X;

      assume

       A1: A0 is maximal_discrete;

      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 discrete non empty TopSpace;

      cluster maximal_discrete -> non proper for SubSpace of X;

      coherence

      proof

        let Y0 be SubSpace of X;

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

        assume Y0 is maximal_discrete;

        then

         A1: A is maximal_discrete;

        A = the carrier of Y0 & A is non proper by A1, Th43;

        hence thesis;

      end;

      cluster proper -> non maximal_discrete for SubSpace of X;

      coherence ;

      cluster non proper -> maximal_discrete for SubSpace of X;

      coherence by Th43;

      cluster non maximal_discrete -> proper for SubSpace of X;

      coherence ;

    end

    registration

      let X be anti-discrete non empty TopSpace;

      cluster maximal_discrete -> trivial for non empty SubSpace of X;

      coherence ;

      cluster non trivial -> non maximal_discrete for non empty SubSpace of X;

      coherence ;

      cluster trivial -> maximal_discrete for non empty SubSpace of X;

      coherence by Th44;

      cluster non maximal_discrete -> non trivial for non empty SubSpace of X;

      coherence ;

    end

    begin

    scheme :: TEX_2:sch1

    ExChoiceFCol { X() -> non empty TopStruct , F() -> Subset-Family of X() , P[ object, object] } :

ex f be Function of F(), the carrier of X() st for S be Subset of X() st S in F() holds P[S, (f . S)]

      provided

       A1: for S be Subset of X() st S in F() holds ex x be Point of X() st P[S, x];

      defpred X[ object, object] means $2 in the carrier of X() & P[$1, $2];

      

       A2: for S be object st S in F() holds ex x be object st x in the carrier of X() & X[S, x]

      proof

        let S be object;

        assume

         A3: S in F();

        then

        reconsider Q = S as Subset of X();

        consider x be Point of X() such that

         A4: P[Q, x] by A1, A3;

        take x;

        thus thesis by A4;

      end;

      consider f be Function such that

       A5: ( dom f) = F() and

       A6: ( rng f) c= the carrier of X() and

       A7: for S be object st S in F() holds X[S, (f . S)] from FUNCT_1:sch 6( A2);

      reconsider f as Function of F(), the carrier of X() by A5, A6, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus thesis by A7;

    end;

    reserve X for almost_discrete non empty TopSpace;

    theorem :: TEX_2:48

    

     Th48: for A be Subset of X holds ( Cl A) = ( union { ( Cl {a}) where a be Point of X : a in A })

    proof

      let A be Subset of X;

      set F = { ( Cl {a}) where a be Point of X : a in A };

      now

        let C be object;

        assume C in F;

        then ex a be Point of X st C = ( Cl {a}) & a in A;

        hence C in ( bool the carrier of X);

      end;

      then

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

      reconsider F as Subset-Family of X;

      now

        let x be object;

        assume

         A1: x in A;

        then

        reconsider a = x as Point of X;

        ( Cl {a}) in F by A1;

        then

         A2: ( Cl {a}) c= ( union F) by ZFMISC_1: 74;

        

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

        a in {a} by TARSKI:def 1;

        then a in ( Cl {a}) by A3;

        hence x in ( union F) by A2;

      end;

      then

       A4: A c= ( union F) by TARSKI:def 3;

      now

        let C be set;

        assume C in F;

        then

        consider a be Point of X such that

         A5: C = ( Cl {a}) and

         A6: a in A;

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

        hence C c= ( Cl A) by A5, PRE_TOPC: 19;

      end;

      then

       A7: ( union F) c= ( Cl A) by ZFMISC_1: 76;

      now

        let G be Subset of X;

        assume G in F;

        then ex a be Point of X st G = ( Cl {a}) & a in A;

        hence G is open by TDLAT_3: 22;

      end;

      then F is open by TOPS_2:def 1;

      then ( union F) is open by TOPS_2: 19;

      then ( union F) is closed by TDLAT_3: 21;

      then ( Cl A) c= ( union F) by A4, TOPS_1: 5;

      hence thesis by A7;

    end;

    theorem :: TEX_2:49

    

     Th49: for a,b be Point of X holds a in ( Cl {b}) implies ( Cl {a}) = ( Cl {b})

    proof

      let a,b be Point of X;

      assume a in ( Cl {b});

      then

       A1: {a} c= ( Cl {b}) by ZFMISC_1: 31;

      b in ( Cl {a})

      proof

        assume not b in ( Cl {a});

        then

         A2: {b} misses ( Cl {a}) by ZFMISC_1: 50;

        ( Cl {a}) is open by TDLAT_3: 22;

        then ( Cl {b}) misses ( Cl {a}) by A2, TSEP_1: 36;

        then (( Cl {b}) /\ ( Cl {a})) = {} ;

        then ( Cl {a}) = {} by A1, TOPS_1: 5, XBOOLE_1: 28;

        hence contradiction by PRE_TOPC: 18, XBOOLE_1: 3;

      end;

      then {b} c= ( Cl {a}) by ZFMISC_1: 31;

      then

       A3: ( Cl {b}) c= ( Cl {a}) by TOPS_1: 5;

      ( Cl {a}) c= ( Cl {b}) by A1, TOPS_1: 5;

      hence thesis by A3;

    end;

    theorem :: TEX_2:50

    

     Th50: for a,b be Point of X holds ( Cl {a}) misses ( Cl {b}) or ( Cl {a}) = ( Cl {b})

    proof

      let a,b be Point of X;

      assume (( Cl {a}) /\ ( Cl {b})) <> {} ;

      then

      consider x be object such that

       A1: x in (( Cl {a}) /\ ( Cl {b})) by XBOOLE_0:def 1;

      reconsider x as Point of X by A1;

      x in ( Cl {a}) by A1, XBOOLE_0:def 4;

      then

       A2: ( Cl {x}) = ( Cl {a}) by Th49;

      x in ( Cl {b}) by A1, XBOOLE_0:def 4;

      hence thesis by A2, Th49;

    end;

    theorem :: TEX_2:51

    

     Th51: for A be Subset of X holds (for x be Point of X st x in A holds ex F be Subset of X st F is closed & (A /\ F) = {x}) implies A is discrete

    proof

      let A be Subset of X;

      assume

       A1: for x be Point of X st x in A holds ex F be Subset of X st F is closed & (A /\ F) = {x};

      now

        let x be Point of X;

        assume

         A2: x in A;

        now

          consider F be Subset of X such that

           A3: F is closed and

           A4: (A /\ F) = {x} by A1, A2;

          take F;

          thus F is open by A3, TDLAT_3: 22;

          thus (A /\ F) = {x} by A4;

        end;

        hence ex G be Subset of X st G is open & (A /\ G) = {x};

      end;

      hence thesis by Th31;

    end;

    theorem :: TEX_2:52

    

     Th52: for A be Subset of X holds (for x be Point of X st x in A holds (A /\ ( Cl {x})) = {x}) implies A is discrete

    proof

      let A be Subset of X;

      assume

       A1: for x be Point of X st x in A holds (A /\ ( Cl {x})) = {x};

      now

        let x be Point of X;

        assume

         A2: x in A;

        now

          take F = ( Cl {x});

          thus F is closed;

          thus (A /\ F) = {x} by A1, A2;

        end;

        hence ex F be Subset of X st F is closed & (A /\ F) = {x};

      end;

      hence thesis by Th51;

    end;

    theorem :: TEX_2:53

    for A be Subset of X holds A is discrete iff for a,b be Point of X st a in A & b in A holds a <> b implies ( Cl {a}) misses ( Cl {b})

    proof

      let A be Subset of X;

      thus A is discrete implies for a,b be Point of X st a in A & b in A holds a <> b implies ( Cl {a}) misses ( Cl {b})

      proof

        assume

         A1: A is discrete;

        let a,b be Point of X;

        assume that

         A2: a in A and

         A3: b in A;

        

         A4: (A /\ ( Cl {b})) = {b} by A1, A3, Th36;

        assume

         A5: a <> b;

        assume (( Cl {a}) /\ ( Cl {b})) <> {} ;

        then

         A6: ( Cl {a}) meets ( Cl {b});

        (A /\ ( Cl {a})) = {a} by A1, A2, Th36;

        then {a} = {b} by A4, A6, Th50;

        hence contradiction by A5, ZFMISC_1: 3;

      end;

      assume

       A7: for a,b be Point of X st a in A & b in A holds a <> b implies ( Cl {a}) misses ( Cl {b});

      now

        let x be Point of X;

        assume

         A8: x in A;

        assume

         A9: (A /\ ( Cl {x})) <> {x};

        

         A10: {x} c= ( Cl {x}) by PRE_TOPC: 18;

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

        then ((A /\ ( Cl {x})) \ {x}) <> {} by A10, A9, Lm3, XBOOLE_1: 19;

        then

        consider y be object such that

         A11: y in ((A /\ ( Cl {x})) \ {x}) by XBOOLE_0:def 1;

        reconsider y as Point of X by A11;

         not y in {x} by A11, XBOOLE_0:def 5;

        then

         A12: y <> x by TARSKI:def 1;

        

         A13: y in (A /\ ( Cl {x})) by A11, XBOOLE_0:def 5;

        then y in A by XBOOLE_0:def 4;

        then ( Cl {y}) misses ( Cl {x}) by A7, A8, A12;

        then

         A14: (( Cl {y}) /\ ( Cl {x})) = {} ;

        y in ( Cl {x}) by A13, XBOOLE_0:def 4;

        then ( Cl {y}) = ( Cl {x}) by Th49;

        hence contradiction by A14, PRE_TOPC: 18, XBOOLE_1: 3;

      end;

      hence thesis by Th52;

    end;

    theorem :: TEX_2:54

    

     Th54: for A be Subset of X holds A is discrete iff for x be Point of X st x in ( Cl A) holds ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a}

    proof

      let A be Subset of X;

      thus A is discrete implies for x be Point of X st x in ( Cl A) holds ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a}

      proof

        assume

         A1: A is discrete;

        let x be Point of X;

        

         A2: ( Cl A) = ( union { ( Cl {a}) where a be Point of X : a in A }) by Th48;

        assume x in ( Cl A);

        then

        consider C be set such that

         A3: x in C and

         A4: C in { ( Cl {a}) where a be Point of X : a in A } by A2, TARSKI:def 4;

        consider a be Point of X such that

         A5: C = ( Cl {a}) and

         A6: a in A by A4;

        now

          take a;

          thus a in A by A6;

          ( Cl {x}) = ( Cl {a}) by A3, A5, Th49;

          hence (A /\ ( Cl {x})) = {a} by A1, A6, Th36;

        end;

        hence thesis;

      end;

      assume

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

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

      proof

        let x be Point of X;

        assume

         A8: x in A;

        A c= ( Cl A) by PRE_TOPC: 18;

        then

         A9: ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a} by A7, A8;

        

         A10: {x} c= ( Cl {x}) by PRE_TOPC: 18;

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

        hence thesis by A9, A10, XBOOLE_1: 19, ZFMISC_1: 18;

      end;

      hence thesis by Th52;

    end;

    theorem :: TEX_2:55

    for A be Subset of X st A is open or A is closed holds A is maximal_discrete implies not A is proper

    proof

      let A be Subset of X;

      assume

       A1: A is open or A is closed;

      then A is closed by TDLAT_3: 21;

      then

       A2: A = ( Cl A) by PRE_TOPC: 22;

      assume

       A3: A is maximal_discrete;

      A is open by A1, TDLAT_3: 22;

      then A is dense by A3, Th41;

      then A = the carrier of X by A2, TOPS_3:def 2;

      hence thesis;

    end;

    theorem :: TEX_2:56

    

     Th56: for A be Subset of X holds A is maximal_discrete implies A is dense

    proof

      let A be Subset of X;

      assume

       A1: A is maximal_discrete;

      then

       A2: A is discrete;

      assume not A is dense;

      then ( Cl A) <> the carrier of X by TOPS_3:def 2;

      then (the carrier of X \ ( Cl A)) <> {} by Lm3;

      then

      consider a be object such that

       A3: a in (the carrier of X \ ( Cl A)) by XBOOLE_0:def 1;

      reconsider a as Point of X by A3;

      set B = (A \/ {a});

      

       A4: A c= B by XBOOLE_1: 7;

       A5:

      now

        let x be Point of X;

        assume x in B;

        then

         A6: x in A or x in {a} by XBOOLE_0:def 3;

        now

          per cases by A6, TARSKI:def 1;

            suppose

             A7: x in A;

            then

            consider G be Subset of X such that

             A8: G is open and

             A9: (A /\ G) = {x} by A2, Th26;

            now

              take E = (( Cl A) /\ G);

              

               A10: (B /\ E) = ((A /\ E) \/ ( {a} /\ E)) by XBOOLE_1: 23;

              ( Cl A) is open by TDLAT_3: 22;

              hence E is open by A8;

              

               A11: {x} c= E by A9, PRE_TOPC: 18, XBOOLE_1: 26;

              E c= ( Cl A) by XBOOLE_1: 17;

              then not a in E by A3, XBOOLE_0:def 5;

              then {a} misses E by ZFMISC_1: 50;

              then

               A12: ( {a} /\ E) = {} ;

               {x} c= B by A4, A7, ZFMISC_1: 31;

              then

               A13: {x} c= (B /\ E) by A11, XBOOLE_1: 19;

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

              hence (B /\ E) = {x} by A9, A13, A12, A10;

            end;

            hence ex E be Subset of X st E is open & (B /\ E) = {x};

          end;

            suppose

             A14: x = a;

            now

              take G = (( [#] X) \ ( Cl A));

              

               A15: (B /\ G) = ((A /\ G) \/ ( {a} /\ G)) by XBOOLE_1: 23;

              

               A16: G = (( Cl A) ` );

              hence G is open;

              A c= ( Cl A) by PRE_TOPC: 18;

              then A misses G by A16, SUBSET_1: 24;

              then

               A17: (A /\ G) = {} ;

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

              hence (B /\ G) = {x} by A14, A17, A15, XBOOLE_1: 28;

            end;

            hence ex G be Subset of X st G is open & (B /\ G) = {x};

          end;

        end;

        hence ex G be Subset of X st G is open & (B /\ G) = {x};

      end;

      A c= ( Cl A) by PRE_TOPC: 18;

      then

       A18: not a in A by A3, XBOOLE_0:def 5;

      ex D be Subset of X st D is discrete & A c= D & A <> D

      proof

        take B;

        thus B is discrete by A5, Th31;

        thus A c= B by XBOOLE_1: 7;

        A <> B by A18, ZFMISC_1: 31, XBOOLE_1: 7;

        hence thesis;

      end;

      hence contradiction by A1;

    end;

    theorem :: TEX_2:57

    

     Th57: for A be Subset of X st A is maximal_discrete holds ( union { ( Cl {a}) where a be Point of X : a in A }) = the carrier of X

    proof

      let A be Subset of X;

      assume A is maximal_discrete;

      then A is dense by Th56;

      then ( Cl A) = the carrier of X by TOPS_3:def 2;

      hence thesis by Th48;

    end;

    theorem :: TEX_2:58

    

     Th58: for A be Subset of X holds A is maximal_discrete iff for x be Point of X holds ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a}

    proof

      let A be Subset of X;

      thus A is maximal_discrete implies for x be Point of X holds ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a}

      proof

        assume

         A1: A is maximal_discrete;

        let x be Point of X;

        the carrier of X = ( union { ( Cl {a}) where a be Point of X : a in A }) by A1, Th57;

        then

        consider C be set such that

         A2: x in C and

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

        consider a be Point of X such that

         A4: C = ( Cl {a}) and

         A5: a in A by A3;

        

         A6: A is discrete by A1;

        now

          take a;

          thus a in A by A5;

          ( Cl {x}) = ( Cl {a}) by A2, A4, Th49;

          hence (A /\ ( Cl {x})) = {a} by A6, A5, Th36;

        end;

        hence thesis;

      end;

      assume

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

      

       A8: for D be Subset of X st D is discrete & A c= D holds A = D

      proof

        let D be Subset of X;

        assume

         A9: D is discrete;

        assume

         A10: A c= D;

        now

          let x be object;

          assume

           A11: x in D;

          then

          reconsider y = x as Point of X;

          

           A12: ex a be Point of X st a in A & (A /\ ( Cl {y})) = {a} by A7;

          (D /\ ( Cl {y})) = {y} by A9, A11, Th36;

          hence x in A by A10, A12, XBOOLE_1: 26, ZFMISC_1: 18;

        end;

        then D c= A by TARSKI:def 3;

        hence thesis by A10;

      end;

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

      proof

        let x be Point of X;

        

         A13: {x} c= ( Cl {x}) by PRE_TOPC: 18;

        assume x in A;

        then

         A14: {x} c= A by ZFMISC_1: 31;

        ex a be Point of X st a in A & (A /\ ( Cl {x})) = {a} by A7;

        hence thesis by A14, A13, XBOOLE_1: 19, ZFMISC_1: 18;

      end;

      then A is discrete by Th52;

      hence A is maximal_discrete by A8;

    end;

    theorem :: TEX_2:59

    

     Th59: for A be Subset of X holds A is discrete implies ex M be Subset of X st A c= M & M is maximal_discrete

    proof

      let A be Subset of X;

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

      set F = { ( Cl {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 = ( Cl {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 discrete;

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

      

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

      then D is closed by TDLAT_3: 21;

      then

       A3: D = ( Cl D) by PRE_TOPC: 22;

      A c= ( Cl A) by PRE_TOPC: 18;

      then A misses D by A2, SUBSET_1: 24;

      then

       A4: (A /\ D) = {} ;

      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 = ( Cl {d}) and

         A7: d in D;

        take d;

         {d} c= ( Cl {d}) by PRE_TOPC: 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 ExChoiceFCol( 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

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

      D misses ( Cl A) by A2, SUBSET_1: 24;

      then

       A10: ( Cl A) misses (f .: F) by A9, XBOOLE_1: 63;

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

      proof

        take M;

        thus

         A11: 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 /\ ( Cl {x})) = {a}

        proof

          let x be Point of X;

          

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

          now

            per cases by A12, XBOOLE_0:def 3;

              suppose

               A13: x in ( Cl A);

              now

                consider a be Point of X such that

                 A14: a in A and

                 A15: (A /\ ( Cl {x})) = {a} by A1, A13, Th54;

                take a;

                thus a in M by A11, A14;

                 {x} c= ( Cl A) by A13, ZFMISC_1: 31;

                then (f .: F) misses ( Cl {x}) by A10, TOPS_1: 5, XBOOLE_1: 63;

                then ((f .: F) /\ ( Cl {x})) = {} ;

                then (M /\ ( Cl {x})) = ((A /\ ( Cl {x})) \/ {} ) by XBOOLE_1: 23;

                hence (M /\ ( Cl {x})) = {a} by A15;

              end;

              hence thesis;

            end;

              suppose

               A16: x in D;

              then

               A17: ( Cl {x}) in F;

              now

                reconsider a = (f . ( Cl {x})) as Point of X by A17, FUNCT_2: 5;

                take a;

                

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

                now

                  let y be object;

                  assume

                   A19: y in (M /\ ( Cl {x}));

                  then

                  reconsider z = y as Point of X;

                  

                   A20: z in ( Cl {x}) by A19, XBOOLE_0:def 4;

                  

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

                   {x} c= D by A16, ZFMISC_1: 31;

                  then ( Cl {x}) c= D by A3, PRE_TOPC: 19;

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

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

                  then

                  consider C be object such that

                   A22: C in F and C in F and

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

                  reconsider C as Subset of X by A22;

                  consider w be Point of X such that

                   A24: C = ( Cl {w}) and w in D by A22;

                  ( Cl {z}) = ( Cl {x}) by A20, Th49;

                  then (f . ( Cl {w})) = a by A8, A22, A23, A24, Th49;

                  hence y in {a} by A23, A24, TARSKI:def 1;

                end;

                then

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

                

                 A26: a in (f .: F) by A17, FUNCT_2: 35;

                hence a in M by A18;

                a in ( Cl {x}) by A8, A17;

                then

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

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

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

                hence (M /\ ( Cl {x})) = {a} by A25;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        hence M is maximal_discrete by Th58;

      end;

    end;

    theorem :: TEX_2:60

    

     Th60: ex M be Subset of X st M is maximal_discrete

    proof

      set A = ( {} X);

      A is discrete by Th29;

      then

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

       A1: M is maximal_discrete by Th59;

      take M;

      thus thesis by A1;

    end;

    theorem :: TEX_2:61

    

     Th61: for Y0 be discrete non empty SubSpace of X holds ex X0 be strict non empty SubSpace of X st Y0 is SubSpace of X0 & X0 is maximal_discrete

    proof

      let Y0 be discrete non empty SubSpace of X;

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

      A is discrete by Th20;

      then

      consider M be Subset of X such that

       A1: A c= M and

       A2: M is maximal_discrete by Th59;

      M is non empty by A2, Th40;

      then

      consider X0 be strict non empty SubSpace of X such that

       A3: X0 is maximal_discrete and

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

      take X0;

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

    end;

    registration

      let X be almost_discrete non discrete non empty TopSpace;

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

      coherence

      proof

        let X0 be non empty SubSpace of X;

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

        assume X0 is maximal_discrete;

        then A is maximal_discrete;

        then A is discrete;

        then

         A1: X0 is discrete by Th20;

        X0 is proper

        proof

          assume X0 is non proper;

          then not A is proper;

          then

           A2: A = the carrier of X;

          X is SubSpace of X by TSEP_1: 2;

          then the TopStruct of X0 = the TopStruct of X by A2, TSEP_1: 5;

          hence contradiction by A1, Th12;

        end;

        hence thesis;

      end;

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

      coherence ;

    end

    registration

      let X be almost_discrete non anti-discrete non empty TopSpace;

      cluster maximal_discrete -> non trivial for non empty SubSpace of X;

      coherence

      proof

        let X0 be non empty SubSpace of X;

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

        assume X0 is maximal_discrete;

        then A is maximal_discrete;

        then A is dense by Th56;

        then

         A1: ( Cl A) = the carrier of X by TOPS_3:def 2;

        assume X0 is trivial;

        then

        consider s be Element of X0 such that

         A2: the carrier of X0 = {s} by SUBSET_1: 46;

        s in A;

        then

        reconsider a = s as Point of X;

        A = {a} by A2;

        then for C be Subset of X, x be Point of X st C = {x} holds ( Cl C) = the carrier of X by A1, Th49;

        hence contradiction by TDLAT_3: 20;

      end;

      cluster trivial -> non maximal_discrete for non empty SubSpace of X;

      coherence ;

    end

    registration

      let X be almost_discrete non empty TopSpace;

      cluster maximal_discrete strict non empty non empty for SubSpace of X;

      existence

      proof

        consider M be Subset of X such that

         A1: M is maximal_discrete by Th60;

        M is non empty by A1, Th40;

        then

        consider X0 be strict non empty SubSpace of X such that

         A2: X0 is maximal_discrete and M = the carrier of X0 by A1, Th47;

        take X0;

        thus thesis by A2;

      end;

    end

    begin

    reserve X,Y for non empty TopSpace;

    theorem :: TEX_2:62

    

     Th62: for X be discrete TopSpace, Y be TopSpace, f be Function of X, Y holds f is continuous by TDLAT_3: 16;

    theorem :: TEX_2:63

    (for Y be non empty TopSpace, f be Function of X, Y holds f is continuous) implies X is discrete

    proof

      set Y = ( 1TopSp the carrier of X);

      reconsider f = ( id the carrier of X) as Function of X, Y;

      assume for Y be non empty TopSpace, f be Function of X, Y holds f is continuous;

      then

       A1: f is continuous;

      for A be Subset of X holds A is closed

      proof

        let A be Subset of X;

        reconsider B = A as Subset of Y;

        

         A2: (f " B) = A by FUNCT_2: 94;

        B is closed by TDLAT_3: 16;

        hence thesis by A1, A2;

      end;

      hence thesis by TDLAT_3: 16;

    end;

    theorem :: TEX_2:64

    for Y be anti-discrete non empty TopSpace, f be Function of X, Y holds f is continuous

    proof

      let Y be anti-discrete non empty TopSpace, f be Function of X, Y;

      now

        let B be Subset of Y;

        assume

         A1: B is closed;

        now

          per cases by A1, TDLAT_3: 19;

            suppose B = {} ;

            then (f " B) = ( {} X);

            hence (f " B) is closed;

          end;

            suppose B = the carrier of Y;

            then B = ( [#] Y);

            then (f " B) = ( [#] X) by TOPS_2: 41;

            hence (f " B) is closed;

          end;

        end;

        hence (f " B) is closed;

      end;

      hence thesis;

    end;

    theorem :: TEX_2:65

    (for X be non empty TopSpace, f be Function of X, Y holds f is continuous) implies Y is anti-discrete

    proof

      set X = ( ADTS the carrier of Y);

      

       A1: X = TopStruct (# the carrier of Y, ( cobool the carrier of Y) #) by TEX_1:def 3;

      then

      reconsider f = ( id the carrier of Y) as Function of X, Y;

      assume for X be non empty TopSpace, f be Function of X, Y holds f is continuous;

      then

       A2: f is continuous;

      for A be Subset of Y st A is closed holds A = {} or A = the carrier of Y

      proof

        let A be Subset of Y;

        reconsider B = A as Subset of X by A1;

        

         A3: (f " A) = B by FUNCT_2: 94;

        assume A is closed;

        then B is closed by A2, A3;

        hence thesis by A1, TDLAT_3: 19;

      end;

      hence thesis by TDLAT_3: 19;

    end;

    reserve X for discrete non empty TopSpace,

X0 for non empty SubSpace of X;

    theorem :: TEX_2:66

    

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

    proof

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

      defpred X[ set, set] means $1 in A implies $2 = $1;

      

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

      consider r be Function of X, X0 such that

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

      reconsider r as continuous Function of X, X0 by Th62;

      take r;

      thus thesis by A2, BORSUK_1:def 16;

    end;

    theorem :: TEX_2:67

    X0 is_a_retract_of X

    proof

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

      hence thesis by BORSUK_1:def 17;

    end;

    reserve X for almost_discrete non empty TopSpace,

X0 for maximal_discrete non empty SubSpace of X;

    theorem :: TEX_2:68

    

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

    proof

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

      defpred X[ Point of X, Point of X0] means (A /\ ( Cl {$1})) = {$2};

      

       A1: A is maximal_discrete by Th45;

      then

       A2: A is discrete;

      

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

         A4: a in A and

         A5: (A /\ ( Cl {x})) = {a} by A1, Th58;

        reconsider a as Point of X0 by A4;

        take a;

        thus thesis by A5;

      end;

      consider r be Function of X, X0 such that

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

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

      proof

        let F be Subset of X0;

        assume F is closed;

        F c= A;

        then

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

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

        now

          let x be object;

          assume

           A7: x in (r " F);

          then

          reconsider b = x as Point of X;

          

           A8: (r . b) in F by A7, FUNCT_2: 38;

          E c= the carrier of X;

          then

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

          ( Cl {a}) in R by A8;

          then

           A9: ( Cl {a}) c= ( union R) by ZFMISC_1: 74;

          (A /\ ( Cl {b})) = {a} by A6;

          then a in (A /\ ( Cl {b})) by ZFMISC_1: 31;

          then a in ( Cl {b}) by XBOOLE_0:def 4;

          then

           A10: ( Cl {a}) = ( Cl {b}) by Th49;

          

           A11: {b} c= ( Cl {b}) by PRE_TOPC: 18;

          b in {b} by TARSKI:def 1;

          then b in ( Cl {a}) by A10, A11;

          hence x in ( union R) by A9;

        end;

        then

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

        now

          let C be set;

          assume C in R;

          then

          consider a be Point of X such that

           A13: C = ( Cl {a}) and

           A14: a in E;

          now

            let x be object;

            assume

             A15: x in C;

            then

            reconsider b = x as Point of X by A13;

            

             A16: (A /\ ( Cl {b})) = {(r . b)} by A6;

            

             A17: (A /\ ( Cl {a})) = {a} by A2, A14, Th36;

            ( Cl {a}) = ( Cl {b}) by A13, A15, Th49;

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

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

          end;

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

        end;

        then

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

        ( Cl E) = ( union R) by Th48;

        hence thesis by A18, A12, XBOOLE_0:def 10;

      end;

      then

      reconsider r as continuous Function of X, X0 by PRE_TOPC:def 6;

      take r;

      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

         A19: (A /\ ( Cl {x})) = {x} by A2, Th36;

        (A /\ ( Cl {x})) = {(r . x)} by A6;

        hence thesis by A19, ZFMISC_1: 3;

      end;

      hence thesis by BORSUK_1:def 16;

    end;

    theorem :: TEX_2:69

    X0 is_a_retract_of X

    proof

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

      hence thesis by BORSUK_1:def 17;

    end;

    

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

    proof

      let r be continuous Function of X, X0;

      assume

       A1: r is being_a_retraction;

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

      assume a = b;

      then

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

      a in {a} by TARSKI:def 1;

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

      then

       A3: {b} c= (r " {a}) by ZFMISC_1: 31;

       {a} is closed by TDLAT_3: 16;

      then (r " {a}) is closed by PRE_TOPC:def 6;

      hence thesis by A3, TOPS_1: 5;

    end;

    theorem :: TEX_2:70

    

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

    proof

      let r be continuous Function of X, X0;

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

      

       A1: A is maximal_discrete by Th45;

      assume

       A2: r is being_a_retraction;

      

       A3: for a be Point of X holds (A /\ ( Cl {a})) = {(r . a)}

      proof

        let a be Point of X;

        

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

        consider c be Point of X such that

         A5: c in A and

         A6: (A /\ ( Cl {a})) = {c} by A1, Th58;

        reconsider b = c as Point of X0 by A5;

         {c} c= ( Cl {a}) by A6, XBOOLE_1: 17;

        then

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

        ( Cl {c}) c= (r " {b}) by A2, Lm4;

        then ( Cl {a}) c= (r " {b}) by A7, Th49;

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

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

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

        hence thesis by A6, TARSKI:def 1;

      end;

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

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

      assume

       A8: F = E;

      now

        let x be object;

        assume

         A9: x in (r " F);

        then

        reconsider b = x as Point of X;

        

         A10: (r . b) in F by A9, FUNCT_2: 38;

        then

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

        ( Cl {a}) in R by A8, A10;

        then

         A11: ( Cl {a}) c= ( union R) by ZFMISC_1: 74;

        

         A12: {b} c= ( Cl {b}) by PRE_TOPC: 18;

        (A /\ ( Cl {b})) = {a} by A3;

        then a in (A /\ ( Cl {b})) by ZFMISC_1: 31;

        then a in ( Cl {b}) by XBOOLE_0:def 4;

        then

         A13: ( Cl {a}) = ( Cl {b}) by Th49;

        b in {b} by TARSKI:def 1;

        then b in ( Cl {a}) by A13, A12;

        hence x in ( union R) by A11;

      end;

      then

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

      

       A15: A is discrete by A1;

      now

        let C be set;

        assume C in R;

        then

        consider a be Point of X such that

         A16: C = ( Cl {a}) and

         A17: a in E;

        now

          let x be object;

          assume

           A18: x in C;

          then

          reconsider b = x as Point of X by A16;

          

           A19: (A /\ ( Cl {b})) = {(r . b)} by A3;

          

           A20: (A /\ ( Cl {a})) = {a} by A8, A15, A17, Th36;

          ( Cl {a}) = ( Cl {b}) by A16, A18, Th49;

          then a = (r . x) by A20, A19, ZFMISC_1: 3;

          hence x in (r " F) by A8, A16, A17, A18, FUNCT_2: 38;

        end;

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

      end;

      then

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

      ( Cl E) = ( union R) by Th48;

      hence thesis by A21, A14;

    end;

    theorem :: TEX_2:71

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

    reserve X0 for discrete non empty SubSpace of X;

    theorem :: TEX_2:72

    

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

    proof

      consider Z0 be strict non empty SubSpace of X such that

       A1: X0 is SubSpace of Z0 and

       A2: Z0 is maximal_discrete by Th61;

      reconsider Z0 as maximal_discrete strict non empty SubSpace of X by A2;

      reconsider Z1 = Z0 as non empty TopSpace;

      reconsider Z1 as discrete non empty TopSpace;

      reconsider X1 = X0 as non empty SubSpace of Z1 by A1;

      consider g be continuous Function of Z1, X1 such that

       A3: g is being_a_retraction by Th66;

      reconsider g as continuous Function of Z0, X0;

      consider h be continuous Function of X, Z0 such that

       A4: h is being_a_retraction by Th68;

      reconsider r = (g * h) as continuous Function of X, X0;

      take r;

      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

         A5: x in the carrier of X0;

        the carrier of X1 c= the carrier of Z1 by BORSUK_1: 1;

        then

        reconsider y = x as Point of Z1 by A5;

        (g . y) = y by A3, A5, BORSUK_1:def 16;

        then (g . (h . x)) = x by A4, BORSUK_1:def 16;

        hence thesis by FUNCT_2: 15;

      end;

      hence thesis by BORSUK_1:def 16;

    end;

    theorem :: TEX_2:73

    X0 is_a_retract_of X

    proof

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

      hence thesis by BORSUK_1:def 17;

    end;