tex_1.miz



    begin

    reserve X for non empty TopSpace,

D for Subset of X;

    theorem :: TEX_1:1

    

     Th1: for B be Subset of X, C be Subset of (X modified_with_respect_to D) st B = C holds B is open implies C is open

    proof

      let B be Subset of X, C be Subset of (X modified_with_respect_to D);

      assume

       A1: B = C;

      

       A2: the topology of X c= (D -extension_of_the_topology_of X) by TMAP_1: 88;

      

       A3: the topology of (X modified_with_respect_to D) = (D -extension_of_the_topology_of X) by TMAP_1: 93;

      assume B in the topology of X;

      hence thesis by A1, A2, A3;

    end;

    theorem :: TEX_1:2

    for B be Subset of X, C be Subset of (X modified_with_respect_to D) st B = C holds B is closed implies C is closed

    proof

      let B be Subset of X, C be Subset of (X modified_with_respect_to D);

      assume

       A1: B = C;

      

       A2: the carrier of (X modified_with_respect_to D) = the carrier of X by TMAP_1: 93;

      assume B is closed;

      then (C ` ) is open by A1, A2, Th1;

      hence thesis;

    end;

    theorem :: TEX_1:3

    

     Th3: for C be Subset of (X modified_with_respect_to (D ` )) st C = D holds C is closed

    proof

      let C be Subset of (X modified_with_respect_to (D ` ));

      assume C = D;

      then (C ` ) = (D ` ) by TMAP_1: 93;

      then (C ` ) is open by TMAP_1: 94;

      hence thesis;

    end;

    theorem :: TEX_1:4

    

     Th4: for C be Subset of (X modified_with_respect_to D) st C = D holds D is dense implies C is dense & C is open

    proof

      let C be Subset of (X modified_with_respect_to D);

      assume

       A1: C = D;

      set A = (( Cl C) ` );

      A in the topology of (X modified_with_respect_to D) by PRE_TOPC:def 2;

      then A in (D -extension_of_the_topology_of X) by TMAP_1: 93;

      then

       A2: A in { (H \/ (G /\ D)) where H be Subset of X, G be Subset of X : H in the topology of X & G in the topology of X } by TMAP_1:def 7;

      reconsider B = A as Subset of X by TMAP_1: 93;

      consider H,G be Subset of X such that

       A3: A = (H \/ (G /\ D)) and

       A4: H in the topology of X and G in the topology of X by A2;

      

       A5: H c= A by A3, XBOOLE_1: 7;

      

       A6: C c= ( Cl C) by PRE_TOPC: 18;

      then D misses A by A1, SUBSET_1: 24;

      then (G /\ D) misses A by XBOOLE_1: 17, XBOOLE_1: 63;

      then

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

      A = ((H \/ (G /\ D)) /\ A) by A3

      .= ((H /\ A) \/ {} ) by A7, XBOOLE_1: 23

      .= (H /\ A);

      then A c= H by XBOOLE_1: 17;

      then B = H by A5, XBOOLE_0:def 10;

      then

       A8: B is open by A4;

      D misses B by A1, A6, SUBSET_1: 24;

      then ( Cl D) misses B by A8, TSEP_1: 36;

      then

       A9: (( Cl D) /\ B) = {} by XBOOLE_0:def 7;

      assume D is dense;

      then

       A10: ( Cl D) = ( [#] X) by TOPS_1:def 3;

      thus C is dense

      proof

        assume not C is dense;

        then ( Cl C) <> ( [#] (X modified_with_respect_to D)) by TOPS_1:def 3;

        then B <> ( {} (X modified_with_respect_to D)) by TOPS_3: 2;

        hence contradiction by A9, A10, XBOOLE_1: 28;

      end;

      thus thesis by A1, TMAP_1: 94;

    end;

    theorem :: TEX_1:5

    

     Th5: for C be Subset of (X modified_with_respect_to D) st D c= C holds D is dense implies C is everywhere_dense

    proof

      let C be Subset of (X modified_with_respect_to D);

      assume

       A1: D c= C;

      reconsider E = D as Subset of (X modified_with_respect_to D) by TMAP_1: 93;

      assume

       A2: D is dense;

      then

       A3: E is open by Th4;

      E is dense by A2, Th4;

      hence thesis by A1, A3, TOPS_3: 36, TOPS_3: 38;

    end;

    theorem :: TEX_1:6

    

     Th6: for C be Subset of (X modified_with_respect_to (D ` )) st C = D holds D is boundary implies C is boundary & C is closed

    proof

      let C be Subset of (X modified_with_respect_to (D ` ));

      assume C = D;

      then

       A1: (C ` ) = (D ` ) by TMAP_1: 93;

      assume D is boundary;

      then

       A2: (D ` ) is dense by TOPS_1:def 4;

      then

       A3: (C ` ) is open by A1, Th4;

      (C ` ) is dense by A1, A2, Th4;

      hence thesis by A3, TOPS_1:def 4;

    end;

    theorem :: TEX_1:7

    

     Th7: for C be Subset of (X modified_with_respect_to (D ` )) st C c= D holds D is boundary implies C is nowhere_dense

    proof

      let C be Subset of (X modified_with_respect_to (D ` ));

      assume

       A1: C c= D;

      reconsider E = D as Subset of (X modified_with_respect_to (D ` )) by TMAP_1: 93;

      assume

       A2: D is boundary;

      then

       A3: E is closed by Th6;

      E is boundary by A2, Th6;

      hence thesis by A1, A3, TOPS_3: 26;

    end;

    

     Lm1: for X,Y be set holds X c= Y iff X is Subset of Y;

    begin

    definition

      let Y be non empty 1-sorted;

      :: original: trivial

      redefine

      :: TEX_1:def1

      attr Y is trivial means

      : Def1: ex d be Element of Y st the carrier of Y = {d};

      compatibility

      proof

        hereby

          assume

           A1: Y is trivial;

          thus ex d be Element of Y st the carrier of Y = {d}

          proof

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

            set d = the Element of Y;

            reconsider D = {d} as Subset of Y;

            take d;

            now

              let a be Element of Y;

              assume a in A;

              a = d by A1;

              hence a in D by TARSKI:def 1;

            end;

            then A c= D by SUBSET_1: 2;

            hence thesis by XBOOLE_0:def 10;

          end;

        end;

        given d be Element of Y such that

         A2: the carrier of Y = {d};

        now

          let a,b be Element of Y;

          a = d by A2, TARSKI:def 1;

          hence a = b by A2, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      cluster 1 -element strict for TopStruct;

      existence

      proof

        set O = the 1 -element 1-sorted;

        reconsider tau = {} as Subset-Family of O by XBOOLE_1: 2;

        reconsider tau as Subset-Family of O;

        take TopStruct (# the carrier of O, tau #);

        thus the carrier of TopStruct (# the carrier of O, tau #) is 1 -element;

        thus thesis;

      end;

      cluster non trivial strict for TopStruct;

      existence

      proof

        set O = the non trivial 1-sorted;

        reconsider tau = {} as Subset-Family of O by XBOOLE_1: 2;

        take TopStruct (# the carrier of O, tau #);

        thus thesis;

      end;

    end

    theorem :: TEX_1:8

    for Y be 1 -element TopStruct st the topology of Y is non empty holds Y is almost_discrete implies Y is TopSpace-like

    proof

      let Y be 1 -element TopStruct;

      consider d be Element of Y such that

       A1: the carrier of Y = {d} by Def1;

      reconsider D = {d} as Subset of Y;

      assume the topology of Y is non empty;

      then

      consider A be Subset of Y such that

       A2: A in the topology of Y by SUBSET_1: 4;

      assume

       A3: for A be Subset of Y st A in the topology of Y holds (the carrier of Y \ A) in the topology of Y;

      

       A4: ( bool D) = { {} , D} by ZFMISC_1: 24;

      now

        per cases by A1, A4, TARSKI:def 2;

          suppose

           A5: A = {} ;

          (D \ A) in the topology of Y by A1, A2, A3;

          hence { {} , D} c= the topology of Y by A2, A5, ZFMISC_1: 32;

        end;

          suppose

           A6: A = D;

          (D \ A) in the topology of Y by A1, A2, A3;

          then {} in the topology of Y by A6, XBOOLE_1: 37;

          hence { {} , D} c= the topology of Y by A2, A6, ZFMISC_1: 32;

        end;

      end;

      then the topology of Y = { {} , the carrier of Y} by A1, A4, XBOOLE_0:def 10;

      then

      reconsider Y as anti-discrete TopStruct by TDLAT_3:def 2;

      Y is TopSpace-like;

      hence thesis;

    end;

    registration

      cluster 1 -element strict for TopSpace;

      existence

      proof

        set O = the 1 -element 1-sorted;

        reconsider tau = ( bool the carrier of O) as Subset-Family of O;

        set Y = TopStruct (# the carrier of O, tau #);

        reconsider Y as discrete non empty TopStruct by TDLAT_3:def 1;

        reconsider Y as TopSpace-like non empty TopStruct;

        take Y;

        thus the carrier of Y is 1 -element;

        thus thesis;

      end;

    end

    registration

      cluster -> anti-discrete discrete for 1 -element TopSpace;

      coherence

      proof

        let Y be 1 -element TopSpace;

        

         A1: the carrier of Y in the topology of Y by PRE_TOPC:def 1;

        ex d be Element of Y st the carrier of Y = {d} by Def1;

        then

         A2: ( bool the carrier of Y) = { {} , the carrier of Y} by ZFMISC_1: 24;

         {} in the topology of Y by PRE_TOPC: 1;

        then { {} , the carrier of Y} c= the topology of Y by A1, ZFMISC_1: 32;

        then the topology of Y = ( bool the carrier of Y) by A2, XBOOLE_0:def 10;

        hence thesis by A2;

      end;

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

      coherence

      proof

        let Y be non empty TopSpace;

        assume Y is discrete anti-discrete;

        then

         A3: ( bool the carrier of Y) = { {} , the carrier of Y};

        now

          set d0 = the Element of Y;

          take d0;

          thus {d0} = the carrier of Y by A3, TARSKI:def 2;

        end;

        hence thesis;

      end;

    end

    registration

      cluster non trivial strict for TopSpace;

      existence

      proof

        set D = { {} , 1};

        reconsider tau = ( bool D) as Subset-Family of D;

        reconsider tau as Subset-Family of D;

        reconsider Y = TopStruct (# D, tau #) as discrete non empty TopStruct by TDLAT_3:def 1;

        take Y;

        now

          assume Y is trivial;

          then

          consider d be Element of Y such that

           A1: the carrier of Y = {d};

          d = {} by A1, ZFMISC_1: 4;

          hence contradiction by A1, ZFMISC_1: 4;

        end;

        hence thesis;

      end;

    end

    registration

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

      coherence ;

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

      coherence ;

    end

    begin

    definition

      let D be set;

      :: TEX_1:def2

      func cobool D -> Subset-Family of D equals { {} , D};

      coherence

      proof

        

         A1: D in ( bool D) by ZFMISC_1:def 1;

         {} c= D by XBOOLE_1: 2;

        hence thesis by A1, ZFMISC_1: 32;

      end;

    end

    registration

      let D be set;

      cluster ( cobool D) -> non empty;

      coherence ;

    end

    definition

      let D be set;

      :: TEX_1:def3

      func ADTS (D) -> TopStruct equals TopStruct (# D, ( cobool D) #);

      coherence ;

    end

    registration

      let D be set;

      cluster ( ADTS D) -> strict anti-discrete TopSpace-like;

      coherence

      proof

        set Y = TopStruct (# D, ( cobool D) #);

        reconsider Y9 = Y as anti-discrete TopStruct by TDLAT_3:def 2;

        Y9 is anti-discrete strict TopSpace;

        hence thesis;

      end;

    end

    registration

      let D be non empty set;

      cluster ( ADTS D) -> non empty;

      coherence ;

    end

    theorem :: TEX_1:9

    

     Th9: for X be anti-discrete non empty TopSpace holds for A be Subset of X holds (A is empty implies ( Cl A) = {} ) & (A is non empty implies ( Cl A) = the carrier of X) by PCOMPS_1: 2, TDLAT_3: 19;

    theorem :: TEX_1:10

    

     Th10: for X be anti-discrete non empty TopSpace holds for A be Subset of X holds (A <> the carrier of X implies ( Int A) = {} ) & (A = the carrier of X implies ( Int A) = the carrier of X)

    proof

      let X be anti-discrete non empty TopSpace;

      let A be Subset of X;

      thus A <> the carrier of X implies ( Int A) = {}

      proof

        assume

         A1: A <> the carrier of X;

        now

          assume ( Int A) = the carrier of X;

          then the carrier of X c= A by TOPS_1: 16;

          hence contradiction by A1, XBOOLE_0:def 10;

        end;

        hence thesis by TDLAT_3: 18;

      end;

      thus A = the carrier of X implies ( Int A) = the carrier of X

      proof

        assume A = the carrier of X;

        then A = ( [#] X);

        hence thesis by TOPS_1: 15;

      end;

    end;

    theorem :: TEX_1:11

    

     Th11: for X be non empty TopSpace holds (for A be Subset of X holds (A is non empty implies ( Cl A) = the carrier of X)) implies X is anti-discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds (A is non empty implies ( Cl A) = the carrier of X);

      now

        let A be Subset of X;

        assume A is closed;

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

        hence A = {} or A = the carrier of X by A1;

      end;

      hence thesis by TDLAT_3: 19;

    end;

    theorem :: TEX_1:12

    

     Th12: for X be non empty TopSpace holds (for A be Subset of X holds (A <> the carrier of X implies ( Int A) = {} )) implies X is anti-discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds (A <> the carrier of X implies ( Int A) = {} );

      now

        let A be Subset of X;

        assume A is open;

        then A = ( Int A) by TOPS_1: 23;

        hence A = {} or A = the carrier of X by A1;

      end;

      hence thesis by TDLAT_3: 18;

    end;

    theorem :: TEX_1:13

    for X be anti-discrete non empty TopSpace holds for A be Subset of X holds (A <> {} implies A is dense) & (A <> the carrier of X implies A is boundary)

    proof

      let X be anti-discrete non empty TopSpace;

      let A be Subset of X;

      thus A <> {} implies A is dense

      proof

        assume A <> {} ;

        then ( Cl A) = the carrier of X by Th9;

        hence thesis by TOPS_3:def 2;

      end;

      thus A <> the carrier of X implies A is boundary

      proof

        assume A <> the carrier of X;

        then ( Int A) = {} by Th10;

        hence thesis by TOPS_1: 48;

      end;

    end;

    theorem :: TEX_1:14

    for X be non empty TopSpace holds (for A be Subset of X holds (A <> {} implies A is dense)) implies X is anti-discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds (A <> {} implies A is dense);

      for A be Subset of X st A is non empty holds ( Cl A) = the carrier of X by A1, TOPS_3:def 2;

      hence thesis by Th11;

    end;

    theorem :: TEX_1:15

    for X be non empty TopSpace holds (for A be Subset of X holds (A <> the carrier of X implies A is boundary)) implies X is anti-discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds (A <> the carrier of X implies A is boundary);

      now

        let A be Subset of X;

        reconsider B = A as Subset of X;

        assume A <> the carrier of X;

        then B is boundary by A1;

        hence ( Int A) = {} ;

      end;

      hence thesis by Th12;

    end;

    registration

      let D be set;

      cluster ( 1TopSp D) -> discrete;

      coherence ;

    end

    theorem :: TEX_1:16

    for X be discrete non empty TopSpace holds for A be Subset of X holds ( Cl A) = A & ( Int A) = A by TDLAT_3: 16, TDLAT_3: 15, PRE_TOPC: 22, TOPS_1: 23;

    theorem :: TEX_1:17

    for X be non empty TopSpace holds (for A be Subset of X holds ( Cl A) = A) implies X is discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds ( Cl A) = A;

      now

        let A be Subset of X;

        ( Cl A) = A by A1;

        hence A is closed;

      end;

      hence thesis by TDLAT_3: 16;

    end;

    theorem :: TEX_1:18

    for X be non empty TopSpace holds (for A be Subset of X holds ( Int A) = A) implies X is discrete

    proof

      let X be non empty TopSpace;

      assume

       A1: for A be Subset of X holds ( Int A) = A;

      now

        let A be Subset of X;

        ( Int A) = A by A1;

        hence A is open;

      end;

      hence thesis by TDLAT_3: 15;

    end;

    theorem :: TEX_1:19

    

     Th19: for D be non empty set holds ( ADTS D) = ( 1TopSp D) iff ex d0 be Element of D st D = {d0}

    proof

      let D be non empty set;

      thus ( ADTS D) = ( 1TopSp D) implies ex d0 be Element of D st D = {d0}

      proof

        set d0 = the Element of D;

        assume

         A1: ( ADTS D) = ( 1TopSp D);

        take d0;

        thus thesis by A1, TARSKI:def 2;

      end;

      given d0 be Element of D such that

       A2: D = {d0};

      thus thesis by A2, ZFMISC_1: 24;

    end;

    registration

      cluster discrete non anti-discrete strict non empty for TopSpace;

      existence

      proof

        set D = { {} , 1};

        set Y = ( 1TopSp D);

        take Y;

        now

          assume Y is anti-discrete;

          then the TopStruct of Y = the TopStruct of ( ADTS D);

          then

          consider d0 be Element of D such that

           A1: D = {d0} by Th19;

          d0 = {} by A1, ZFMISC_1: 4;

          hence contradiction by A1, ZFMISC_1: 4;

        end;

        hence thesis;

      end;

      cluster anti-discrete non discrete strict non empty for TopSpace;

      existence

      proof

        set D = { {} , 1};

        set Y = ( ADTS D);

        take Y;

        now

          assume Y is discrete;

          then the TopStruct of Y = the TopStruct of ( 1TopSp D);

          then

          consider d0 be Element of D such that

           A2: D = {d0} by Th19;

          d0 = {} by A2, ZFMISC_1: 4;

          hence contradiction by A2, ZFMISC_1: 4;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let D be set, d0 be Element of D;

      :: TEX_1:def4

      func STS (D,d0) -> TopStruct equals TopStruct (# D, (( bool D) \ { A where A be Subset of D : d0 in A & A <> D }) #);

      coherence ;

    end

    registration

      let D be set, d0 be Element of D;

      cluster ( STS (D,d0)) -> strict TopSpace-like;

      coherence

      proof

        reconsider E = D as Subset of D by Lm1;

        set G = { A where A be Subset of D : d0 in A & A <> D };

        set T = (( bool D) \ G);

        set Y = TopStruct (# D, T #);

        thus ( STS (D,d0)) is strict;

         not ex A be Subset of D st A = E & d0 in A & A <> D;

        then

         A1: not E in G;

         A2:

        now

          let F be Subset-Family of Y;

          assume F c= the topology of Y;

          then F misses G by XBOOLE_1: 63, XBOOLE_1: 79;

          then

           A3: (F /\ G) = {} by XBOOLE_0:def 7;

          now

            per cases ;

              case ( union F) = D;

              hence ( union F) in the topology of Y by A1, XBOOLE_0:def 5;

            end;

              case

               A4: ( union F) <> D;

               A5:

              now

                let A be Subset of D;

                assume

                 A6: A in F;

                assume A = D;

                then D c= ( union F) by A6, ZFMISC_1: 74;

                hence contradiction by A4, XBOOLE_0:def 10;

              end;

              now

                let A be set;

                assume

                 A7: A in F;

                then

                reconsider B = A as Subset of D;

                 not B in G by A3, A7, XBOOLE_0:def 4;

                then not (d0 in B & B <> D);

                hence not d0 in A by A5, A7;

              end;

              then not ex A be set st d0 in A & A in F;

              then not ex A be Subset of D st A = ( union F) & d0 in A & A <> D by TARSKI:def 4;

              then not ( union F) in G;

              hence ( union F) in the topology of Y by XBOOLE_0:def 5;

            end;

          end;

          hence ( union F) in the topology of Y;

        end;

         A8:

        now

          let C,E be Subset of Y;

          assume that

           A9: C in the topology of Y and

           A10: E in the topology of Y;

           A11:

          now

            let P be Subset of D;

            assume that

             A12: P in the topology of Y and

             A13: P <> D;

             not P in G by A12, XBOOLE_0:def 5;

            hence not d0 in P by A13;

          end;

          now

            per cases ;

              case C = D & E = D;

              hence (C /\ E) in the topology of Y by A1, XBOOLE_0:def 5;

            end;

              case

               A14: C <> D or E <> D;

              now

                per cases by A14;

                  case

                   A15: C <> D;

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

                  then not ex A be Subset of D st A = (C /\ E) & d0 in A & A <> D by A9, A11, A15;

                  then not (C /\ E) in G;

                  hence (C /\ E) in the topology of Y by XBOOLE_0:def 5;

                end;

                  case

                   A16: E <> D;

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

                  then not ex A be Subset of D st A = (C /\ E) & d0 in A & A <> D by A10, A11, A16;

                  then not (C /\ E) in G;

                  hence (C /\ E) in the topology of Y by XBOOLE_0:def 5;

                end;

              end;

              hence (C /\ E) in the topology of Y;

            end;

          end;

          hence (C /\ E) in the topology of Y;

        end;

        the carrier of Y in the topology of Y by A1, XBOOLE_0:def 5;

        hence thesis by A2, A8;

      end;

    end

    registration

      let D be non empty set, d0 be Element of D;

      cluster ( STS (D,d0)) -> non empty;

      coherence ;

    end

    reserve D for non empty set,

d0 for Element of D;

    theorem :: TEX_1:20

    

     Th20: for A be Subset of ( STS (D,d0)) holds ( {d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A)

    proof

      let A be Subset of ( STS (D,d0));

      set Z = (A ` );

      set G = { P where P be Subset of D : d0 in P & P <> D };

      thus {d0} c= A implies A is closed

      proof

        

         A1: d0 in {d0} by TARSKI:def 1;

        assume {d0} c= A;

        then not ex Q be Subset of D st Q = Z & d0 in Q & Q <> D by A1, XBOOLE_0:def 5;

        then not Z in G;

        then Z in the topology of ( STS (D,d0)) by XBOOLE_0:def 5;

        then Z is open;

        hence thesis;

      end;

      assume A is non empty;

      then

       A2: Z <> D by TOPS_3: 1;

      assume A is closed;

      then Z in the topology of ( STS (D,d0)) by PRE_TOPC:def 2;

      then not Z in G by XBOOLE_0:def 5;

      then not d0 in Z by A2;

      then d0 in A by SUBSET_1: 29;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: TEX_1:21

    

     Th21: (D \ {d0}) is non empty implies for A be Subset of ( STS (D,d0)) holds (A = {d0} implies A is closed & A is boundary) & (A is non empty & A is closed & A is boundary implies A = {d0})

    proof

      assume

       A1: (D \ {d0}) is non empty;

      set G = { P where P be Subset of D : d0 in P & P <> D };

      let A be Subset of ( STS (D,d0));

      

       A2: ( Int A) in the topology of ( STS (D,d0)) by PRE_TOPC:def 2;

      thus A = {d0} implies A is closed & A is boundary

      proof

        assume

         A3: A = {d0};

        hence A is closed by Th20;

         A4:

        now

          assume

           A5: ( Int A) = A;

          then

           A6: d0 in ( Int A) by A3, TARSKI:def 1;

          ( Int A) <> D by A1, A3, A5, XBOOLE_1: 37;

          then ( Int A) in G by A6;

          hence contradiction by A2, XBOOLE_0:def 5;

        end;

        ( Int A) c= A by TOPS_1: 16;

        then ( Int A) = {} or ( Int A) = A by A3, ZFMISC_1: 33;

        hence thesis by A4, TOPS_1: 48;

      end;

      thus A is non empty & A is closed & A is boundary implies A = {d0}

      proof

        set Z = (A \ {d0});

        assume that

         A7: A is non empty and

         A8: A is closed;

        

         A9: {d0} c= A by A7, A8, Th20;

        

         A10: Z c= A by XBOOLE_1: 36;

        reconsider Z as Subset of ( STS (D,d0));

        d0 in {d0} by TARSKI:def 1;

        then not ex Q be Subset of D st Q = Z & d0 in Q & Q <> D by XBOOLE_0:def 5;

        then not Z in G;

        then Z in the topology of ( STS (D,d0)) by XBOOLE_0:def 5;

        then

         A11: Z is open;

        assume A is boundary;

        then

         A12: ( Int A) = {} ;

        assume

         A13: A <> {d0};

        now

          assume Z = {} ;

          then A c= {d0} by XBOOLE_1: 37;

          hence contradiction by A9, A13, XBOOLE_0:def 10;

        end;

        hence contradiction by A10, A12, A11, TOPS_1: 24, XBOOLE_1: 3;

      end;

    end;

    theorem :: TEX_1:22

    

     Th22: for A be Subset of ( STS (D,d0)) holds (A c= (D \ {d0}) implies A is open) & (A <> D & A is open implies A c= (D \ {d0}))

    proof

      let A be Subset of ( STS (D,d0));

      set Z = (A ` );

      reconsider P = {d0} as Subset of ( STS (D,d0));

      thus A c= (D \ {d0}) implies A is open

      proof

        assume A c= (D \ {d0});

        then (( [#] ( STS (D,d0))) \ (D \ {d0})) c= (( [#] ( STS (D,d0))) \ A) by XBOOLE_1: 34;

        then P c= Z by PRE_TOPC: 3;

        then Z is closed by Th20;

        hence thesis by TOPS_1: 4;

      end;

      thus A <> D & A is open implies A c= (D \ {d0})

      proof

        assume A <> D;

        then

         A1: Z <> ( {} ( STS (D,d0))) by TOPS_3: 2;

        assume A is open;

        then {d0} c= Z by A1, Th20;

        then (Z ` ) c= (P ` ) by SUBSET_1: 12;

        hence thesis;

      end;

    end;

    theorem :: TEX_1:23

    (D \ {d0}) is non empty implies for A be Subset of ( STS (D,d0)) holds (A = (D \ {d0}) implies A is open & A is dense) & (A <> D & A is open & A is dense implies A = (D \ {d0}))

    proof

      assume

       A1: (D \ {d0}) is non empty;

      reconsider P = {d0} as Subset of ( STS (D,d0));

      let A be Subset of ( STS (D,d0));

      set Z = (A ` );

      thus A = (D \ {d0}) implies A is open & A is dense

      proof

        assume

         A2: A = (D \ {d0});

        hence A is open by Th22;

        (( [#] ( STS (D,d0))) \ (( [#] ( STS (D,d0))) \ P)) = Z by A2;

        then P = Z by PRE_TOPC: 3;

        then Z is boundary by A1, Th21;

        hence thesis by TOPS_3: 18;

      end;

      thus A <> D & A is open & A is dense implies A = (D \ {d0})

      proof

        assume A <> D;

        then

         A3: Z <> ( {} ( STS (D,d0))) by TOPS_3: 2;

        assume

         A4: A is open;

        assume A is dense;

        then Z is boundary by TOPS_3: 18;

        then Z = {d0} by A1, A3, A4, Th21;

        then A = (P ` );

        hence thesis;

      end;

    end;

    registration

      cluster non anti-discrete non discrete strict non empty for TopSpace;

      existence

      proof

        set D = { {} , 1};

        reconsider a = {} as Element of D by TARSKI:def 2;

        set Y = ( STS (D,a));

        take Y;

        reconsider A = {a} as non empty Subset of Y;

        

         A1: not 1 in A by TARSKI:def 1;

        1 in D by TARSKI:def 2;

        then

         A2: (D \ A) is non empty by A1, XBOOLE_0:def 5;

        then A is boundary by Th21;

        then ( Int A) <> A;

        then

         A3: not A is open by TOPS_1: 23;

        A is closed by A2, Th21;

        hence thesis by A3, TDLAT_3: 19;

      end;

    end

    theorem :: TEX_1:24

    

     Th24: for Y be non empty TopSpace holds the TopStruct of Y = the TopStruct of ( STS (D,d0)) iff the carrier of Y = D & for A be Subset of Y holds ( {d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A)

    proof

      let Y be non empty TopSpace;

      thus the TopStruct of Y = the TopStruct of ( STS (D,d0)) implies the carrier of Y = D & for A be Subset of Y holds ( {d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A) by TOPS_3: 79, Th20;

      assume

       A1: the carrier of Y = D;

      assume

       A2: for A be Subset of Y holds ( {d0} c= A implies A is closed) & (A is non empty & A is closed implies {d0} c= A);

      now

        let A be Subset of Y, C be Subset of ( STS (D,d0));

        assume

         A3: A = C;

         A4:

        now

          assume

           A5: C is closed;

          now

            per cases ;

              case C = {} ;

              hence A is closed by A3;

            end;

              case C <> {} ;

              then {d0} c= A by A3, A5, Th20;

              hence A is closed by A2;

            end;

          end;

          hence A is closed;

        end;

        now

          assume

           A6: A is closed;

          now

            per cases ;

              case A = {} ;

              hence C is closed by A3;

            end;

              case A <> {} ;

              then {d0} c= C by A2, A3, A6;

              hence C is closed by Th20;

            end;

          end;

          hence C is closed;

        end;

        hence A is closed iff C is closed by A4;

      end;

      hence thesis by A1, TOPS_3: 73;

    end;

    theorem :: TEX_1:25

    

     Th25: for Y be non empty TopSpace holds the TopStruct of Y = the TopStruct of ( STS (D,d0)) iff the carrier of Y = D & for A be Subset of Y holds (A c= (D \ {d0}) implies A is open) & (A <> D & A is open implies A c= (D \ {d0}))

    proof

      let Y be non empty TopSpace;

      thus the TopStruct of Y = the TopStruct of ( STS (D,d0)) implies the carrier of Y = D & for A be Subset of Y holds (A c= (D \ {d0}) implies A is open) & (A <> D & A is open implies A c= (D \ {d0})) by Th22, TOPS_3: 76;

      assume

       A1: the carrier of Y = D;

      assume

       A2: for A be Subset of Y holds (A c= (D \ {d0}) implies A is open) & (A <> D & A is open implies A c= (D \ {d0}));

      now

        let A be Subset of Y, C be Subset of ( STS (D,d0));

        assume

         A3: A = C;

         A4:

        now

          assume

           A5: A is open;

          now

            per cases ;

              case A = D;

              then C = ( [#] ( STS (D,d0))) by A3;

              hence C is open;

            end;

              case A <> D;

              then A c= (D \ {d0}) by A2, A5;

              hence C is open by A3, Th22;

            end;

          end;

          hence C is open;

        end;

        now

          assume

           A6: C is open;

          now

            per cases ;

              case C = D;

              then A = ( [#] Y) by A1, A3;

              hence A is open;

            end;

              case C <> D;

              then A c= (D \ {d0}) by A3, A6, Th22;

              hence A is open by A2;

            end;

          end;

          hence A is open;

        end;

        hence A is open iff C is open by A4;

      end;

      hence thesis by A1, TOPS_3: 72;

    end;

    theorem :: TEX_1:26

    for Y be non empty TopSpace holds the TopStruct of Y = the TopStruct of ( STS (D,d0)) iff the carrier of Y = D & for A be non empty Subset of Y holds ( Cl A) = (A \/ {d0})

    proof

      let Y be non empty TopSpace;

      thus the TopStruct of Y = the TopStruct of ( STS (D,d0)) implies the carrier of Y = D & for A be non empty Subset of Y holds ( Cl A) = (A \/ {d0})

      proof

        assume

         A1: the TopStruct of Y = the TopStruct of ( STS (D,d0));

        hence the carrier of Y = D;

        reconsider P = {d0} as Subset of Y by A1;

        now

          let A be non empty Subset of Y;

          reconsider B = A as Subset of Y;

          ( Cl A) is non empty by PCOMPS_1: 2;

          then

           A2: {d0} c= ( Cl A) by A1, Th24;

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

          then

           A3: (A \/ {d0}) c= ( Cl A) by A2, XBOOLE_1: 8;

           {d0} c= (A \/ P) by XBOOLE_1: 7;

          then (B \/ P) is closed by A1, Th24;

          then

           A4: ( Cl (A \/ P)) = (A \/ {d0}) by PRE_TOPC: 22;

          ( Cl A) c= ( Cl (A \/ P)) by PRE_TOPC: 19, XBOOLE_1: 7;

          hence ( Cl A) = (A \/ {d0}) by A4, A3, XBOOLE_0:def 10;

        end;

        hence thesis;

      end;

      assume

       A5: the carrier of Y = D;

      assume

       A6: for A be non empty Subset of Y holds ( Cl A) = (A \/ {d0});

      now

        let A be Subset of Y;

        thus {d0} c= A implies A is closed

        proof

          assume {d0} c= A;

          then A = (A \/ {d0}) by XBOOLE_1: 12;

          then ( Cl A) = A by A6;

          hence thesis;

        end;

        thus A is non empty & A is closed implies {d0} c= A

        proof

          assume A is non empty;

          then

           A7: ( Cl A) = (A \/ {d0}) by A6;

          assume A is closed;

          then

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

          assume not {d0} c= A;

          hence contradiction by A7, A8, XBOOLE_1: 7;

        end;

      end;

      hence thesis by A5, Th24;

    end;

    theorem :: TEX_1:27

    for Y be non empty TopSpace holds the TopStruct of Y = the TopStruct of ( STS (D,d0)) iff the carrier of Y = D & for A be Subset of Y st A <> D holds ( Int A) = (A \ {d0})

    proof

      let Y be non empty TopSpace;

      thus the TopStruct of Y = the TopStruct of ( STS (D,d0)) implies the carrier of Y = D & for A be Subset of Y st A <> D holds ( Int A) = (A \ {d0})

      proof

        assume

         A1: the TopStruct of Y = the TopStruct of ( STS (D,d0));

        hence the carrier of Y = D;

        reconsider P = {d0} as Subset of Y by A1;

        now

          let A be Subset of Y;

          reconsider B = A as Subset of Y;

          

           A2: A = (A /\ D) by A1, XBOOLE_1: 28;

          assume

           A3: A <> D;

          now

            assume ( Int A) = D;

            then D c= A by TOPS_1: 16;

            hence contradiction by A1, A3, XBOOLE_0:def 10;

          end;

          then

           A4: ( Int A) c= (D \ P) by A1, Th25;

          (A \ {d0}) c= (D \ {d0}) by A1, XBOOLE_1: 33;

          then (B \ P) is open by A1, Th25;

          then ( Int (A \ P)) = (A \ P) by TOPS_1: 23;

          then

           A5: (A \ {d0}) c= ( Int A) by TOPS_1: 19, XBOOLE_1: 36;

          ( Int A) c= A by TOPS_1: 16;

          then ( Int A) c= (A /\ (D \ P)) by A4, XBOOLE_1: 19;

          then ( Int A) c= (A \ {d0}) by A2, XBOOLE_1: 49;

          hence ( Int A) = (A \ {d0}) by A5, XBOOLE_0:def 10;

        end;

        hence thesis;

      end;

      assume

       A6: the carrier of Y = D;

      assume

       A7: for A be Subset of Y st A <> D holds ( Int A) = (A \ {d0});

      now

        let A be Subset of Y;

        thus A c= (D \ {d0}) implies A is open

        proof

          assume

           A8: A c= (D \ {d0});

           A9:

          now

            (D /\ {d0}) = {d0} by ZFMISC_1: 46;

            then

             A10: D meets {d0} by XBOOLE_0:def 7;

            assume A = D;

            then D = (D \ {d0}) by A8, XBOOLE_0:def 10;

            hence contradiction by A10, XBOOLE_1: 83;

          end;

          

           A11: A = (A /\ D) by A6, XBOOLE_1: 28;

          A = (A /\ (D \ {d0})) by A8, XBOOLE_1: 28;

          then A = (A \ {d0}) by A11, XBOOLE_1: 49;

          then ( Int A) = A by A7, A9;

          hence thesis;

        end;

        thus A <> D & A is open implies A c= (D \ {d0})

        proof

          assume

           A12: A <> D;

          assume A is open;

          then ( Int A) = A by TOPS_1: 23;

          then (A \ {d0}) = A by A7, A12;

          hence thesis by A6, XBOOLE_1: 33;

        end;

      end;

      hence thesis by A6, Th25;

    end;

     Lm2:

    now

      let D be non empty set, d0 be Element of D, G be set;

      assume

       A1: G = { P where P be Subset of D : d0 in P & P <> D };

      set x = the Element of G;

      assume

       A2: D = {d0};

      assume G <> {} ;

      then x in G;

      then

      consider S be Subset of D such that x = S and

       A3: d0 in S and

       A4: S <> D by A1;

      set d1 = the Element of (D \ S);

       A5:

      now

        assume (D \ S) = {} ;

        then D c= S by XBOOLE_1: 37;

        hence contradiction by A4, XBOOLE_0:def 10;

      end;

      then

      reconsider d1 as Element of D by XBOOLE_0:def 5;

      d0 <> d1 by A3, A5, XBOOLE_0:def 5;

      hence contradiction by A2, TARSKI:def 1;

    end;

    theorem :: TEX_1:28

    ( STS (D,d0)) = ( ADTS D) iff D = {d0}

    proof

      set G = { P where P be Subset of D : d0 in P & P <> D };

      thus ( STS (D,d0)) = ( ADTS D) implies D = {d0}

      proof

        set d1 = the Element of (D \ {d0});

        assume

         A1: ( STS (D,d0)) = ( ADTS D);

        assume

         A2: D <> {d0};

         A3:

        now

          assume (D \ {d0}) = {} ;

          then D c= {d0} by XBOOLE_1: 37;

          hence contradiction by A2, XBOOLE_0:def 10;

        end;

        then

        reconsider d1 as Element of D by XBOOLE_0:def 5;

        reconsider P = {d1} as Subset of D;

        

         A4: d0 <> d1 by A3, ZFMISC_1: 56;

        then not ex Q be Subset of D st Q = P & d0 in Q & Q <> D by TARSKI:def 1;

        then not P in G;

        then

         A5: P in { {} , D} by A1, XBOOLE_0:def 5;

         {d0} c= D;

        then {d0} c= {d1} by A5, TARSKI:def 2;

        hence contradiction by A4, ZFMISC_1: 18;

      end;

      assume

       A6: D = {d0};

      then G = {} by Lm2;

      hence thesis by A6, ZFMISC_1: 24;

    end;

    theorem :: TEX_1:29

    ( STS (D,d0)) = ( 1TopSp D) iff D = {d0}

    proof

      set G = { P where P be Subset of D : d0 in P & P <> D };

      thus ( STS (D,d0)) = ( 1TopSp D) implies D = {d0}

      proof

        now

          let x be object;

          assume x in G;

          then ex Q be Subset of D st x = Q & d0 in Q & Q <> D;

          hence x in ( bool D);

        end;

        then

         A1: G c= ( bool D) by TARSKI:def 3;

        reconsider P = {d0} as Subset of D;

        assume

         A2: ( STS (D,d0)) = ( 1TopSp D);

        

         A3: d0 in P by TARSKI:def 1;

        assume D <> {d0};

        then P in G by A3;

        hence contradiction by A2, A1, XBOOLE_1: 38;

      end;

      assume D = {d0};

      then G = {} by Lm2;

      hence thesis;

    end;

    theorem :: TEX_1:30

    for D be non empty set, d0 be Element of D holds for A be Subset of ( STS (D,d0)) st A = {d0} holds ( 1TopSp D) = (( STS (D,d0)) modified_with_respect_to A)

    proof

      let D be non empty set, d0 be Element of D;

      set G = { P where P be Subset of D : d0 in P & P <> D };

      set T = (( bool D) \ G);

      let A be Subset of ( STS (D,d0));

      assume

       A1: A = {d0};

      

       A2: (A -extension_of_the_topology_of ( STS (D,d0))) = { (H \/ (F /\ A)) where H be Subset of ( STS (D,d0)), F be Subset of ( STS (D,d0)) : H in T & F in T } by TMAP_1:def 7;

      now

        reconsider F = D as Subset of D by Lm1;

        let W be object;

        assume W in G;

        then

        consider P be Subset of D such that

         A3: W = P and

         A4: d0 in P and P <> D;

        set H = (P \ {d0});

        reconsider H as Subset of D;

        A c= P by A1, A4, ZFMISC_1: 31;

        then

         A5: W = (H \/ A) by A1, A3, XBOOLE_1: 45;

         not ex K be Subset of D st K = F & d0 in K & K <> D;

        then not F in G;

        then

         A6: F in T by XBOOLE_0:def 5;

        d0 in {d0} by TARSKI:def 1;

        then not ex K be Subset of D st K = H & d0 in K & K <> D by XBOOLE_0:def 5;

        then not H in G;

        then

         A7: H in T by XBOOLE_0:def 5;

        A = (F /\ A) by XBOOLE_1: 28;

        hence W in (A -extension_of_the_topology_of ( STS (D,d0))) by A2, A6, A7, A5;

      end;

      then

       A8: G c= (A -extension_of_the_topology_of ( STS (D,d0))) by TARSKI:def 3;

      (T \/ G) = (( bool D) \/ G) by XBOOLE_1: 39;

      then

       A9: ( bool D) c= (T \/ G) by XBOOLE_1: 7;

      T c= (A -extension_of_the_topology_of ( STS (D,d0))) by TMAP_1: 88;

      then (T \/ G) c= (A -extension_of_the_topology_of ( STS (D,d0))) by A8, XBOOLE_1: 8;

      then

       A10: ( bool D) c= (A -extension_of_the_topology_of ( STS (D,d0))) by A9, XBOOLE_1: 1;

      the topology of (( STS (D,d0)) modified_with_respect_to A) = (A -extension_of_the_topology_of ( STS (D,d0))) by TMAP_1: 93

      .= the topology of ( 1TopSp D) by A10, XBOOLE_0:def 10;

      hence thesis by TMAP_1: 93;

    end;

    begin

    definition

      let X be non empty TopSpace;

      :: original: discrete

      redefine

      :: TEX_1:def5

      attr X is discrete means for A be non empty Subset of X holds not A is boundary;

      compatibility

      proof

        hereby

          assume

           A1: X is discrete;

          let A be non empty Subset of X;

          assume A is boundary;

          then ( Int A) <> A;

          then not A is open by TOPS_1: 23;

          hence contradiction by A1;

        end;

        assume

         A2: for A be non empty Subset of X holds not A is boundary;

        now

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

          assume

           A3: A = {x};

          hereby

            per cases ;

              suppose A = {} ;

              hence A is open;

            end;

              suppose A <> {} ;

              then not A is boundary by A2;

              then

               A4: ( Int A) <> {} by TOPS_1: 48;

              ( Int A) c= {x} by A3, TOPS_1: 16;

              hence A is open by A3, A4, ZFMISC_1: 33;

            end;

          end;

        end;

        hence thesis by TDLAT_3: 17;

      end;

    end

    theorem :: TEX_1:31

    X is discrete iff for A be Subset of X holds A <> the carrier of X implies not A is dense

    proof

      hereby

        assume

         A1: X is discrete;

        assume not for A be Subset of X holds A <> the carrier of X implies not A is dense;

        then

        consider A be Subset of X such that

         A2: A <> the carrier of X and

         A3: A is dense;

        now

          reconsider B = (A ` ) as non empty Subset of X by A2, TOPS_3: 2;

          take B;

          thus B is boundary by A3, TOPS_3: 18;

        end;

        hence contradiction by A1;

      end;

      assume

       A4: for C be Subset of X holds C <> the carrier of X implies not C is dense;

      assume X is non discrete;

      then

      consider A be non empty Subset of X such that

       A5: A is boundary;

      now

        take B = (A ` );

        thus B <> the carrier of X & B is dense by A5, TOPS_1:def 4, TOPS_3: 1;

      end;

      hence contradiction by A4;

    end;

    registration

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

      coherence ;

    end

    definition

      let X be non empty TopSpace;

      :: original: almost_discrete

      redefine

      :: TEX_1:def6

      attr X is almost_discrete means for A be non empty Subset of X holds not A is nowhere_dense;

      compatibility

      proof

        hereby

          assume

           A1: X is almost_discrete;

          let A be non empty Subset of X;

          ( Cl A) is open by A1, TDLAT_3: 22;

          then ( Cl A) = ( Int ( Cl A)) by TOPS_1: 23;

          then ( Int ( Cl A)) <> {} by PRE_TOPC: 18, XBOOLE_1: 3;

          hence not A is nowhere_dense by TOPS_3:def 3;

        end;

        assume

         A2: for A be non empty Subset of X holds not A is nowhere_dense;

        now

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

          assume A = {x};

          hereby

            ( Fr ( Cl A)) = {} by A2;

            then (( Cl A) \ ( Int ( Cl A))) = {} by TOPS_1: 43;

            then

             A3: ( Cl A) c= ( Int ( Cl A)) by XBOOLE_1: 37;

            ( Int ( Cl A)) c= ( Cl A) by TOPS_1: 16;

            hence ( Cl A) is open by A3, XBOOLE_0:def 10;

          end;

        end;

        hence thesis by TDLAT_3: 25;

      end;

    end

    theorem :: TEX_1:32

    

     Th32: X is almost_discrete iff for A be Subset of X holds A <> the carrier of X implies not A is everywhere_dense

    proof

      hereby

        assume

         A1: X is almost_discrete;

        assume not for A be Subset of X holds A <> the carrier of X implies not A is everywhere_dense;

        then

        consider A be Subset of X such that

         A2: A is everywhere_dense and

         A3: A <> the carrier of X;

        now

          reconsider B = (A ` ) as non empty Subset of X by A3, TOPS_3: 2;

          take B;

          thus B is nowhere_dense by A2, TOPS_3: 39;

        end;

        hence contradiction by A1;

      end;

      assume

       A4: for A be Subset of X holds A <> the carrier of X implies not A is everywhere_dense;

      assume X is non almost_discrete;

      then

      consider A be non empty Subset of X such that

       A5: A is nowhere_dense;

      now

        take B = (A ` );

        thus B <> the carrier of X & B is everywhere_dense by A5, TOPS_3: 1, TOPS_3: 40;

      end;

      hence contradiction by A4;

    end;

    theorem :: TEX_1:33

    

     Th33: X is non almost_discrete iff ex A be non empty Subset of X st A is boundary & A is closed

    proof

      thus X is non almost_discrete implies ex A be non empty Subset of X st A is boundary & A is closed

      proof

        assume X is non almost_discrete;

        then

        consider A be non empty Subset of X such that

         A1: A is nowhere_dense;

        consider C be Subset of X such that

         A2: A c= C and

         A3: C is closed and

         A4: C is boundary by A1, TOPS_3: 27;

        reconsider C as non empty Subset of X by A2;

        reconsider C as non empty Subset of X;

        take C;

        thus thesis by A3, A4;

      end;

      given A be non empty Subset of X such that

       A5: A is boundary and

       A6: A is closed;

      thus thesis by A5, A6;

    end;

    theorem :: TEX_1:34

    X is non almost_discrete iff ex A be Subset of X st A <> the carrier of X & A is dense & A is open

    proof

      thus X is non almost_discrete implies ex A be Subset of X st A <> the carrier of X & A is dense & A is open

      proof

        assume X is non almost_discrete;

        then

        consider A be non empty Subset of X such that

         A1: A is boundary and

         A2: A is closed by Th33;

        take (A ` );

        thus thesis by A1, A2, TOPS_3: 1;

      end;

      given A be Subset of X such that

       A3: A <> the carrier of X and

       A4: A is dense and

       A5: A is open;

      now

        reconsider B = (A ` ) as non empty Subset of X by A3, TOPS_3: 2;

        take B;

        thus B is boundary & B is closed by A4, A5, TOPS_3: 18;

      end;

      hence thesis;

    end;

    registration

      cluster almost_discrete non discrete non anti-discrete strict non empty for TopSpace;

      existence

      proof

        set C = ( bool { {} , 1});

        set Y = ( ADTS C);

        

         A1: 1 in { {} , 1} by TARSKI:def 2;

         {} in { {} , 1} by TARSKI:def 2;

        then

        reconsider B0 = { {} }, B1 = {1} as Subset of { {} , 1} by A1, ZFMISC_1: 31;

        

         A2: {} c= { {} , 1} by XBOOLE_1: 2;

        then

        reconsider A = { {} } as Subset of Y by ZFMISC_1: 31;

        set Y1 = (Y modified_with_respect_to A);

        

         A3: the carrier of Y1 = the carrier of Y by TMAP_1: 93;

        reconsider A1 = A as Subset of Y1 by TMAP_1: 93;

        set Y2 = (Y1 modified_with_respect_to (A1 ` ));

        reconsider A2 = A1 as Subset of Y2 by TMAP_1: 93;

        set A3 = (A2 ` );

        

         A4: the carrier of Y2 = the carrier of Y1 by TMAP_1: 93;

        then

        reconsider B = {B0, B1} as non empty Subset of Y2 by TMAP_1: 93;

        now

          let H be object;

          assume H in the topology of Y1;

          then H in (A -extension_of_the_topology_of Y) by TMAP_1: 93;

          then H in { (p \/ (q /\ A)) where p,q be Subset of Y : p in the topology of Y & q in the topology of Y } by TMAP_1:def 7;

          then

          consider P,Q be Subset of Y such that

           A5: H = (P \/ (Q /\ A)) and

           A6: P in the topology of Y and

           A7: Q in the topology of Y;

          now

            per cases by A6, A7, TARSKI:def 2;

              case P = {} & Q = {} ;

              hence H = {} by A5;

            end;

              case P = C & Q = {} ;

              hence H = C by A5;

            end;

              case P = {} & Q = C;

              hence H = A by A5, XBOOLE_1: 28;

            end;

              case P = C & Q = C;

              hence H = C by A5, XBOOLE_1: 12;

            end;

          end;

          hence H in { {} , A1, C} by ENUMSET1:def 1;

        end;

        then

         A8: the topology of Y1 c= { {} , A1, C} by TARSKI:def 3;

        now

          let H be object;

          assume H in the topology of Y2;

          then H in ((A1 ` ) -extension_of_the_topology_of Y1) by TMAP_1: 93;

          then H in { (P \/ (Q /\ (A1 ` ))) where P,Q be Subset of Y1 : P in the topology of Y1 & Q in the topology of Y1 } by TMAP_1:def 7;

          then

          consider P,Q be Subset of Y1 such that

           A9: H = (P \/ (Q /\ (A1 ` ))) and

           A10: P in the topology of Y1 and

           A11: Q in the topology of Y1;

          now

            per cases by A8, A10, A11, ENUMSET1:def 1;

              case P = {} & Q = {} ;

              hence H = {} by A9;

            end;

              case P = A1 & Q = {} ;

              hence H = A1 by A9;

            end;

              case P = C & Q = {} ;

              hence H = C by A9;

            end;

              case

               A12: P = {} & Q = A1;

              A1 misses (A1 ` ) by XBOOLE_1: 79;

              hence H = {} by A9, A12, XBOOLE_0:def 7;

            end;

              case

               A13: P = A1 & Q = A1;

              A1 misses (A1 ` ) by XBOOLE_1: 79;

              then (A1 /\ (A1 ` )) = ( {} Y1) by XBOOLE_0:def 7;

              hence H = A1 by A9, A13;

            end;

              case

               A14: P = C & Q = A1;

              A1 misses (A1 ` ) by XBOOLE_1: 79;

              then (A1 /\ (A1 ` )) = ( {} Y1) by XBOOLE_0:def 7;

              hence H = C by A9, A14;

            end;

              case P = {} & Q = C;

              hence H = (A2 ` ) by A3, A4, A9, XBOOLE_1: 28;

            end;

              case

               A15: P = A1 & Q = C;

              (A1 \/ (A1 ` )) = ( [#] Y1) by PRE_TOPC: 2;

              hence H = C by A3, A9, A15, XBOOLE_1: 28;

            end;

              case P = C & Q = C;

              hence H = C by A3, A9, XBOOLE_1: 12;

            end;

          end;

          hence H in { {} , A2, A3, C} by ENUMSET1:def 2;

        end;

        then

         A16: the topology of Y2 c= { {} , A2, A3, C} by TARSKI:def 3;

        

         A17: A2 is open by Th1, TMAP_1: 94;

        

         A18: A2 is closed by Th3;

        now

          let H be object;

          assume H in { {} , A2, A3, C};

          then H = {} or H = A2 or H = A3 or H = C by ENUMSET1:def 2;

          hence H in the topology of Y2 by A3, A4, A18, A17, PRE_TOPC: 1, PRE_TOPC:def 2;

        end;

        then { {} , A2, A3, C} c= the topology of Y2 by TARSKI:def 3;

        then

         A19: the topology of Y2 = { {} , A2, A3, C} by A16, XBOOLE_0:def 10;

         A20:

        now

          let G be Subset of Y2;

          

           A21: G = {} or G = C implies G is closed by A4, TMAP_1: 93;

           A22:

          now

            A3 in the topology of Y2 by A19, ENUMSET1:def 2;

            then

             A23: A3 is open;

            assume G = A2;

            hence G is closed by A23;

          end;

           A24:

          now

            A2 in the topology of Y2 by A19, ENUMSET1:def 2;

            then

             A25: (A3 ` ) is open;

            assume G = A3;

            hence G is closed by A25;

          end;

          assume G is open;

          then G in { {} , A2, A3, C} by A19;

          hence G is closed by A21, A22, A24, ENUMSET1:def 2;

        end;

        

         A26: {} in C by A2;

         A27:

        now

           A28:

          now

            reconsider I = { {} , 1} as Point of Y2 by A3, A4, ZFMISC_1:def 1;

            

             A29: not I in A2 by TARSKI:def 1;

            

             A30: ( Int B) c= B by TOPS_1: 16;

            assume ( Int B) = A3;

            then I in ( Int B) by A29, SUBSET_1: 29;

            then I = B0 or I = B1 by A30, TARSKI:def 2;

            then 1 in B0 or {} in B1 by TARSKI:def 2;

            hence contradiction by TARSKI:def 1;

          end;

          take B;

           A31:

          now

            assume ( Int B) = A2;

            then

             A32: {} in ( Int B) by TARSKI:def 1;

            ( Int B) c= B by TOPS_1: 16;

            hence contradiction by A32, TARSKI:def 2;

          end;

           A33:

          now

            assume ( Int B) = C;

            then C c= B by TOPS_1: 16;

            hence contradiction by A26, TARSKI:def 2;

          end;

          ( Int B) in { {} , A2, A3, C} by A19, PRE_TOPC:def 2;

          then ( Int B) = {} or ( Int B) = A2 or ( Int B) = A3 or ( Int B) = C by ENUMSET1:def 2;

          hence B is boundary by A33, A31, A28, TOPS_1: 48;

        end;

        take Y2;

        now

          take A2;

          now

            assume A2 = C;

            then B0 = {} by TARSKI:def 1;

            hence contradiction;

          end;

          hence A2 is open & A2 <> {} & A2 <> the carrier of Y2 by A4, Th1, TMAP_1: 93, TMAP_1: 94;

        end;

        hence thesis by A27, A20, TDLAT_3: 18, TDLAT_3: 21;

      end;

    end

    theorem :: TEX_1:35

    

     Th35: for C be non empty set, c0 be Element of C holds (C \ {c0}) is non empty iff ( STS (C,c0)) is non almost_discrete

    proof

      let C be non empty set, c0 be Element of C;

      hereby

        assume

         A1: (C \ {c0}) is non empty;

        now

          reconsider A = {c0} as non empty Subset of ( STS (C,c0));

          take A;

          

           A2: A is boundary by A1, Th21;

          A is closed by A1, Th21;

          hence A is nowhere_dense by A2;

        end;

        hence ( STS (C,c0)) is non almost_discrete;

      end;

      assume ( STS (C,c0)) is non almost_discrete;

      then

      consider A be non empty Subset of ( STS (C,c0)) such that

       A3: A is nowhere_dense;

      assume (C \ {c0}) is empty;

      then C c= {c0} by XBOOLE_1: 37;

      then C = {c0} by XBOOLE_0:def 10;

      then A = C by ZFMISC_1: 33;

      hence contradiction by A3, TOPS_3: 23;

    end;

    registration

      cluster non almost_discrete strict non empty for TopSpace;

      existence

      proof

        set D = { {} , 1};

        reconsider a = {} as Element of D by TARSKI:def 2;

        set Y = ( STS (D,a));

        take Y;

        reconsider A = {a} as non empty Subset of Y;

        

         A1: not 1 in A by TARSKI:def 1;

        1 in D by TARSKI:def 2;

        then (D \ A) is non empty by A1, XBOOLE_0:def 5;

        hence thesis by Th35;

      end;

    end

    theorem :: TEX_1:36

    for A be non empty Subset of X st A is boundary holds (X modified_with_respect_to (A ` )) is non almost_discrete

    proof

      let A be non empty Subset of X;

      set Z = (X modified_with_respect_to (A ` ));

      assume

       A1: A is boundary;

      now

        reconsider C = A as non empty Subset of Z by TMAP_1: 93;

        take C;

        thus C is nowhere_dense by A1, Th7;

      end;

      hence thesis;

    end;

    theorem :: TEX_1:37

    for A be Subset of X st A <> the carrier of X & A is dense holds (X modified_with_respect_to A) is non almost_discrete

    proof

      let A be Subset of X;

      assume

       A1: A <> the carrier of X;

      set Z = (X modified_with_respect_to A);

      assume

       A2: A is dense;

      now

        reconsider C = A as Subset of Z by TMAP_1: 93;

        take C;

        thus C <> the carrier of Z & C is everywhere_dense by A1, A2, Th5, TMAP_1: 93;

      end;

      hence thesis by Th32;

    end;