topgen_3.miz



    begin

    reserve a,b,c for set;

    definition

      let X be set;

      let B be Subset-Family of X;

      :: TOPGEN_3:def1

      attr B is point-filtered means for x,U1,U2 be set st U1 in B & U2 in B & x in (U1 /\ U2) holds ex U be Subset of X st U in B & x in U & U c= (U1 /\ U2);

    end

    theorem :: TOPGEN_3:1

    

     Th1: for X be set, B be Subset-Family of X holds B is covering iff for x be set st x in X holds ex U be Subset of X st U in B & x in U

    proof

      let X be set;

      let B be Subset-Family of X;

      hereby

        assume B is covering;

        then

         A1: ( union B) = X by ABIAN: 4;

        let x be set;

        assume x in X;

        then

        consider U be set such that

         A2: x in U and

         A3: U in B by A1, TARSKI:def 4;

        reconsider U as Subset of X by A3;

        take U;

        thus U in B & x in U by A2, A3;

      end;

      assume

       A4: for x be set st x in X holds ex U be Subset of X st U in B & x in U;

      ( union B) = X

      proof

        thus ( union B) c= X;

        let a be object;

        assume a in X;

        then ex U be Subset of X st U in B & a in U by A4;

        hence thesis by TARSKI:def 4;

      end;

      hence thesis by ABIAN: 4;

    end;

    theorem :: TOPGEN_3:2

    

     Th2: for X be set, B be Subset-Family of X st B is point-filtered covering holds for T be TopStruct st the carrier of T = X & the topology of T = ( UniCl B) holds T is TopSpace & B is Basis of T

    proof

      let X be set;

      let B be Subset-Family of X such that

       A1: B is point-filtered covering;

      let T be TopStruct such that

       A2: the carrier of T = X and

       A3: the topology of T = ( UniCl B);

      T is TopSpace-like

      proof

        ( union B) in ( UniCl B) by CANTOR_1:def 1;

        hence the carrier of T in the topology of T by A1, A2, A3, ABIAN: 4;

        hereby

          let a be Subset-Family of T;

          assume a c= the topology of T;

          then ( union a) in ( UniCl the topology of T) by CANTOR_1:def 1;

          hence ( union a) in the topology of T by A2, A3, YELLOW_9: 15;

        end;

        let a,b be Subset of T;

        set Bc = { c where c be Subset of T : c in B & c c= (a /\ b) };

        Bc c= ( bool X)

        proof

          let x be object;

          assume x in Bc;

          then ex c be Subset of T st x = c & c in B & c c= (a /\ b);

          hence thesis;

        end;

        then

        reconsider Bc as Subset-Family of T by A2;

        assume a in the topology of T;

        then

        consider Ba be Subset-Family of T such that

         A4: Ba c= B and

         A5: a = ( union Ba) by A2, A3, CANTOR_1:def 1;

        assume b in the topology of T;

        then

        consider Bb be Subset-Family of T such that

         A6: Bb c= B and

         A7: b = ( union Bb) by A2, A3, CANTOR_1:def 1;

        

         A8: ( union Bc) = (a /\ b)

        proof

          Bc c= ( bool (a /\ b))

          proof

            let x be object;

            assume x in Bc;

            then ex c be Subset of T st x = c & c in B & c c= (a /\ b);

            hence thesis;

          end;

          then ( union Bc) c= ( union ( bool (a /\ b))) by ZFMISC_1: 77;

          hence ( union Bc) c= (a /\ b) by ZFMISC_1: 81;

          let x be object;

          assume

           A9: x in (a /\ b);

          then x in a by XBOOLE_0:def 4;

          then

          consider U1 be set such that

           A10: x in U1 and

           A11: U1 in Ba by A5, TARSKI:def 4;

          x in b by A9, XBOOLE_0:def 4;

          then

          consider U2 be set such that

           A12: x in U2 and

           A13: U2 in Bb by A7, TARSKI:def 4;

          

           A14: U2 c= b by A7, A13, ZFMISC_1: 74;

          x in (U1 /\ U2) by A10, A12, XBOOLE_0:def 4;

          then

          consider U be Subset of X such that

           A15: U in B and

           A16: x in U and

           A17: U c= (U1 /\ U2) by A4, A11, A6, A13, A1;

          U1 c= a by A5, A11, ZFMISC_1: 74;

          then (U1 /\ U2) c= (a /\ b) by A14, XBOOLE_1: 27;

          then U c= (a /\ b) by A17;

          then U in Bc by A2, A15;

          hence thesis by A16, TARSKI:def 4;

        end;

        Bc c= B

        proof

          let x be object;

          assume x in Bc;

          then ex c be Subset of T st x = c & c in B & c c= (a /\ b);

          hence thesis;

        end;

        hence thesis by A8, A2, A3, CANTOR_1:def 1;

      end;

      hence T is TopSpace;

      reconsider B9 = B as Subset-Family of T by A2;

      B9 c= the topology of T by A3, CANTOR_1: 1;

      hence thesis by A2, A3, CANTOR_1:def 2, TOPS_2: 64;

    end;

    theorem :: TOPGEN_3:3

    for X be set, B be non-empty ManySortedSet of X st ( rng B) c= ( bool ( bool X)) & (for x,U be set st x in X & U in (B . x) holds x in U) & (for x,y,U be set st x in U & U in (B . y) & y in X holds ex V be set st V in (B . x) & V c= U) & (for x,U1,U2 be set st x in X & U1 in (B . x) & U2 in (B . x) holds ex U be set st U in (B . x) & U c= (U1 /\ U2)) holds ex P be Subset-Family of X st P = ( Union B) & for T be TopStruct st the carrier of T = X & the topology of T = ( UniCl P) holds T is TopSpace & for T9 be non empty TopSpace st T9 = T holds B is Neighborhood_System of T9

    proof

      let X be set;

      let B be non-empty ManySortedSet of X such that

       A1: ( rng B) c= ( bool ( bool X));

      ( Union B) c= ( union ( bool ( bool X))) by A1, ZFMISC_1: 77;

      then

      reconsider P = ( Union B) as Subset-Family of X by ZFMISC_1: 81;

      

       A2: ( dom B) = X by PARTFUN1:def 2;

      assume

       A3: for x,U be set st x in X & U in (B . x) holds x in U;

      assume

       A4: for x,y,U be set st x in U & U in (B . y) & y in X holds ex V be set st V in (B . x) & V c= U;

      assume

       A5: for x,U1,U2 be set st x in X & U1 in (B . x) & U2 in (B . x) holds ex U be set st U in (B . x) & U c= (U1 /\ U2);

      

       A6: P is point-filtered

      proof

        let x,U1,U2 be set;

        assume that

         A7: U1 in P and

         A8: U2 in P and

         A9: x in (U1 /\ U2);

        

         A10: x in U2 by A9, XBOOLE_0:def 4;

        ex y2 be object st y2 in X & U2 in (B . y2) by A2, A8, CARD_5: 2;

        then

        consider V2 be set such that

         A11: V2 in (B . x) and

         A12: V2 c= U2 by A10, A4;

        

         A13: x in U1 by A9, XBOOLE_0:def 4;

        ex y1 be object st y1 in X & U1 in (B . y1) by A7, A2, CARD_5: 2;

        then

        consider V1 be set such that

         A14: V1 in (B . x) and

         A15: V1 c= U1 by A13, A4;

        

         A16: x in X by A2, A14, FUNCT_1:def 2;

        then

        consider U be set such that

         A17: U in (B . x) and

         A18: U c= (V1 /\ V2) by A5, A14, A11;

        U in P by A2, A16, A17, CARD_5: 2;

        then

        reconsider U as Subset of X;

        take U;

        thus U in P by A2, A16, A17, CARD_5: 2;

        thus x in U by A3, A16, A17;

        (V1 /\ V2) c= (U1 /\ U2) by A15, A12, XBOOLE_1: 27;

        hence thesis by A18;

      end;

      take P;

      thus P = ( Union B);

      let T be TopStruct such that

       A19: the carrier of T = X and

       A20: the topology of T = ( UniCl P);

      now

        let x be set;

        set U = the Element of (B . x);

        assume

         A21: x in X;

        then

         A22: U in P by A2, CARD_5: 2;

        x in U by A3, A21;

        hence ex U be Subset of X st U in P & x in U by A22;

      end;

      then P is covering by Th1;

      hence T is TopSpace by A19, A20, A6, Th2;

      let T9 be non empty TopSpace;

      assume

       A23: T9 = T;

      then

      reconsider B9 = B as ManySortedSet of T9 by A19;

      B9 is Neighborhood_System of T9

      proof

        let x be Point of T9;

        

         A24: (B9 . x) in ( rng B) by A2, A19, A23, FUNCT_1:def 3;

        then

        reconsider Bx = (B9 . x) as Subset-Family of T9 by A1, A19, A23;

        Bx is Basis of x

        proof

          

           A25: P c= ( UniCl P) by CANTOR_1: 1;

          Bx c= P by A24, ZFMISC_1: 74;

          then Bx c= the topology of T9 by A25, A20, A23;

          then

           A26: Bx is open by TOPS_2: 64;

          Bx is x -quasi_basis

          proof

            for a st a in Bx holds x in a by A3, A19, A23;

            hence x in ( Intersect Bx) by SETFAM_1: 43;

            let A be Subset of T9;

            assume A in the topology of T9;

            then

            consider Y be Subset-Family of T9 such that

             A27: Y c= P and

             A28: A = ( union Y) by A19, A20, A23, CANTOR_1:def 1;

            assume x in A;

            then

            consider a such that

             A29: x in a and

             A30: a in Y by A28, TARSKI:def 4;

            ex b be object st b in ( dom B) & a in (B . b) by A27, A30, CARD_5: 2;

            then

             A31: ex V be set st V in (B . x) & V c= a by A4, A29;

            a c= A by A28, A30, ZFMISC_1: 74;

            hence thesis by A31, XBOOLE_1: 1;

          end;

          hence thesis by A26;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_3:4

    

     Th4: for X be set, F be Subset-Family of X st {} in F & (for A,B be set st A in F & B in F holds (A \/ B) in F) & (for G be Subset-Family of X st G c= F holds ( Intersect G) in F) holds for T be TopStruct st the carrier of T = X & the topology of T = ( COMPLEMENT F) holds T is TopSpace & for A be Subset of T holds A is closed iff A in F

    proof

      let X be set;

      let F be Subset-Family of X;

      assume

       A1: {} in F;

      set O = ( COMPLEMENT F);

      assume

       A2: for A,B be set st A in F & B in F holds (A \/ B) in F;

      assume

       A3: for G be Subset-Family of X st G c= F holds ( Intersect G) in F;

      let T be TopStruct such that

       A4: the carrier of T = X and

       A5: the topology of T = O;

      T is TopSpace-like

      proof

        (( {} T) ` ) in O by A1, A4, SETFAM_1: 35;

        hence the carrier of T in the topology of T by A5;

        hereby

          let a be Subset-Family of T;

          assume a c= the topology of T;

          then ( COMPLEMENT a) c= F by A4, A5, SETFAM_1: 37;

          then ( Intersect ( COMPLEMENT a)) in F by A3, A4;

          then (( union a) ` ) in F by YELLOW_8: 6;

          hence ( union a) in the topology of T by A4, A5, SETFAM_1:def 7;

        end;

        let a,b be Subset of T;

        assume that

         A6: a in the topology of T and

         A7: b in the topology of T;

        

         A8: (b ` ) in F by A7, A4, A5, SETFAM_1:def 7;

        (a ` ) in F by A6, A4, A5, SETFAM_1:def 7;

        then ((a ` ) \/ (b ` )) in F by A8, A2;

        then ((a /\ b) ` ) in F by XBOOLE_1: 54;

        hence thesis by A4, A5, SETFAM_1:def 7;

      end;

      hence T is TopSpace;

      let A be Subset of T;

      A is closed iff (A ` ) is open;

      then A is closed iff (A ` ) in O by A5;

      hence thesis by A4, SETFAM_1: 35;

    end;

    scheme :: TOPGEN_3:sch1

    TopDefByClosedPred { X() -> set , C[ set] } :

ex T be strict TopSpace st the carrier of T = X() & for A be Subset of T holds A is closed iff C[A]

      provided

       A1: C[ {} ] & C[X()]

       and

       A2: for A,B be set st C[A] & C[B] holds C[(A \/ B)]

       and

       A3: for G be Subset-Family of X() st for A be set st A in G holds C[A] holds C[( Intersect G)];

      set X = X();

      set F = { A where A be Subset of X : C[A] };

      F c= ( bool X)

      proof

        let a be object;

        assume a in F;

        then ex B be Subset of X st a = B & C[B];

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of X;

      set T = TopStruct (# X, ( COMPLEMENT F) #);

      

       A4: for A,B be set st A in F & B in F holds (A \/ B) in F

      proof

        let A,B be set;

        assume A in F;

        then

        consider A9 be Subset of X such that

         A5: A = A9 and

         A6: C[A9];

        assume B in F;

        then

        consider B9 be Subset of X such that

         A7: B = B9 and

         A8: C[B9];

        C[(A9 \/ B9)] by A2, A6, A8;

        hence thesis by A5, A7;

      end;

      

       A9: for G be Subset-Family of X st G c= F holds ( Intersect G) in F

      proof

        let G be Subset-Family of X;

        assume

         A10: G c= F;

        now

          let A be set;

          assume A in G;

          then A in F by A10;

          then ex B be Subset of X st A = B & C[B];

          hence C[A];

        end;

        then C[( Intersect G)] by A3;

        hence thesis;

      end;

       {} c= X;

      then

       A11: {} in F by A1;

      then

      reconsider T as strict TopSpace by A9, A4, Th4;

      take T;

      thus the carrier of T = X();

      let A be Subset of T;

      A in F iff ex B be Subset of X st A = B & C[B];

      hence thesis by A11, A4, A9, Th4;

    end;

    

     Lm1: for T1,T2 be TopSpace st for A be set holds A is open Subset of T1 iff A is open Subset of T2 holds the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2

    proof

      let T1,T2 be TopSpace such that

       A1: for A be set holds A is open Subset of T1 iff A is open Subset of T2;

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

      then

       A2: the carrier of T2 is Subset of T1 by A1;

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

      then

       A3: the carrier of T1 is Subset of T2 by A1;

      hence the carrier of T1 = the carrier of T2 by A2;

      let a be object;

      assume

       A4: a in the topology of T1;

      then

      reconsider a as Subset of T1;

      reconsider b = a as Subset of T2 by A3, A2, XBOOLE_0:def 10;

      a is open by A4;

      then b is open by A1;

      hence thesis;

    end;

    theorem :: TOPGEN_3:5

    for T1,T2 be TopSpace st for A be set holds A is open Subset of T1 iff A is open Subset of T2 holds the TopStruct of T1 = the TopStruct of T2

    proof

      let T1,T2 be TopSpace such that

       A1: for A be set holds A is open Subset of T1 iff A is open Subset of T2;

      

       A2: the topology of T2 c= the topology of T1 by A1, Lm1;

      the topology of T1 c= the topology of T2 by A1, Lm1;

      then the topology of T1 = the topology of T2 by A2;

      hence thesis by A1, Lm1;

    end;

    

     Lm2: for T1,T2 be TopSpace st for A be set holds A is closed Subset of T1 iff A is closed Subset of T2 holds the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2

    proof

      let T1,T2 be TopSpace such that

       A1: for A be set holds A is closed Subset of T1 iff A is closed Subset of T2;

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

      then

       A2: the carrier of T2 is Subset of T1 by A1;

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

      then

       A3: the carrier of T1 is Subset of T2 by A1;

      hence

       A4: the carrier of T1 = the carrier of T2 by A2;

      let a be object;

      assume

       A5: a in the topology of T1;

      then

      reconsider a as Subset of T1;

      reconsider b = a as Subset of T2 by A3, A2, XBOOLE_0:def 10;

      a is open by A5;

      then (b ` ) is closed by A1, A4;

      then b is open by TOPS_1: 4;

      hence thesis;

    end;

    theorem :: TOPGEN_3:6

    

     Th6: for T1,T2 be TopSpace st for A be set holds A is closed Subset of T1 iff A is closed Subset of T2 holds the TopStruct of T1 = the TopStruct of T2

    proof

      let T1,T2 be TopSpace such that

       A1: for A be set holds A is closed Subset of T1 iff A is closed Subset of T2;

      

       A2: the topology of T2 c= the topology of T1 by A1, Lm2;

      the topology of T1 c= the topology of T2 by A1, Lm2;

      then the topology of T1 = the topology of T2 by A2;

      hence thesis by A1, Lm2;

    end;

    definition

      let X,Y be set;

      let r be Subset of [:X, ( bool Y):];

      :: original: rng

      redefine

      func rng r -> Subset-Family of Y ;

      coherence by RELAT_1:def 19;

    end

    theorem :: TOPGEN_3:7

    

     Th7: for X be set, c be Function of ( bool X), ( bool X) st (c . {} ) = {} & (for A be Subset of X holds A c= (c . A)) & (for A,B be Subset of X holds (c . (A \/ B)) = ((c . A) \/ (c . B))) & (for A be Subset of X holds (c . (c . A)) = (c . A)) holds for T be TopStruct st the carrier of T = X & the topology of T = ( COMPLEMENT ( rng c)) holds T is TopSpace & for A be Subset of T holds ( Cl A) = (c . A)

    proof

      let X be set;

      let c be Function of ( bool X), ( bool X);

      assume that

       A1: (c . {} ) = {} and

       A2: for A be Subset of X holds A c= (c . A) and

       A3: for A,B be Subset of X holds (c . (A \/ B)) = ((c . A) \/ (c . B)) and

       A4: for A be Subset of X holds (c . (c . A)) = (c . A);

      set F = ( rng c);

      

       A5: ( dom c) = ( bool X) by FUNCT_2:def 1;

       A6:

      now

        let A,B be set;

        assume that

         A7: A in F and

         A8: B in F;

        consider a be object such that

         A9: a in ( dom c) and

         A10: A = (c . a) by A7, FUNCT_1:def 3;

        consider b be object such that

         A11: b in ( dom c) and

         A12: B = (c . b) by A8, FUNCT_1:def 3;

        reconsider a, b as Subset of X by A9, A11;

        (A \/ B) = ((c . A) \/ B) by A4, A9, A10

        .= ((c . A) \/ (c . B)) by A4, A11, A12

        .= (c . ((c . a) \/ (c . b))) by A3, A10, A12;

        hence (A \/ B) in F by A5, FUNCT_1:def 3;

      end;

       A13:

      now

        let A,B be Subset of X;

        assume A c= B;

        then (A \/ B) = B by XBOOLE_1: 12;

        then (c . B) = ((c . A) \/ (c . B)) by A3;

        hence (c . A) c= (c . B) by XBOOLE_1: 11;

      end;

       A14:

      now

        let G be Subset-Family of X such that

         A15: G c= F;

        now

          let a;

          assume

           A16: a in G;

          then

          reconsider A = a as Subset of X;

          

           A17: (c . ( Intersect G)) c= (c . A) by A13, A16, MSSUBFAM: 2;

          ex b be object st b in ( dom c) & A = (c . b) by A15, A16, FUNCT_1:def 3;

          hence (c . ( Intersect G)) c= a by A17, A4;

        end;

        then

         A18: (c . ( Intersect G)) c= ( Intersect G) by MSSUBFAM: 4;

        ( Intersect G) c= (c . ( Intersect G)) by A2;

        then (c . ( Intersect G)) = ( Intersect G) by A18;

        hence ( Intersect G) in F by A5, FUNCT_1:def 3;

      end;

      let T be TopStruct such that

       A19: the carrier of T = X and

       A20: the topology of T = ( COMPLEMENT F);

       {} = ( {} X);

      then

       A21: {} in F by A1, A5, FUNCT_1:def 3;

      hence

       A22: T is TopSpace by A14, A19, A20, A6, Th4;

      let A be Subset of T;

      reconsider B = A, ClA = ( Cl A) as Subset of X by A19;

      reconsider cB = (c . B) as Subset of T by A19;

      cB in F by A5, FUNCT_1:def 3;

      then cB is closed by A19, A20, A21, A6, A14, Th4;

      hence ( Cl A) c= (c . A) by A2, TOPS_1: 5;

      ClA in F by A22, A19, A20, A21, A6, A14, Th4;

      then ex a be object st a in ( dom c) & ClA = (c . a) by FUNCT_1:def 3;

      then (c . ClA) = ClA by A4;

      hence thesis by A19, A13, PRE_TOPC: 18;

    end;

    scheme :: TOPGEN_3:sch2

    TopDefByClosureOp { X() -> set , ClOp( object) -> set } :

ex T be strict TopSpace st the carrier of T = X() & for A be Subset of T holds ( Cl A) = ClOp(A)

      provided

       A1: ClOp({}) = {}

       and

       A2: for A be Subset of X() holds A c= ClOp(A) & ClOp(A) c= X()

       and

       A3: for A,B be Subset of X() holds ClOp(\/) = (ClOp(A) \/ ClOp(B))

       and

       A4: for A be Subset of X() holds ClOp(ClOp) = ClOp(A);

      set X = X();

      consider c be Function such that

       A5: ( dom c) = ( bool X) & for a st a in ( bool X) holds (c . a) = ClOp(a) from FUNCT_1:sch 5;

      now

        let a be object;

        assume

         A6: a in ( bool X);

        then

         A7: ClOp(a) c= X by A2;

        (c . a) = ClOp(a) by A6, A5;

        hence (c . a) in ( bool X) by A7;

      end;

      then

      reconsider c as Function of ( bool X), ( bool X) by A5, FUNCT_2: 3;

      

       A8: for A be Subset of X holds A c= (c . A)

      proof

        let A be Subset of X;

        (c . A) = ClOp(A) by A5;

        hence thesis by A2;

      end;

      

       A9: for A,B be Subset of X holds (c . (A \/ B)) = ((c . A) \/ (c . B))

      proof

        let A,B be Subset of X;

        

         A10: (c . B) = ClOp(B) by A5;

        

         A11: ClOp(\/) = (c . (A \/ B)) by A5;

        (c . A) = ClOp(A) by A5;

        hence thesis by A10, A11, A3;

      end;

      

       A12: for A be Subset of X holds (c . (c . A)) = (c . A)

      proof

        let A be Subset of X;

        

         A13: ClOp(.) = (c . (c . A)) by A5;

        (c . A) = ClOp(A) by A5;

        hence thesis by A13, A4;

      end;

       {} c= X;

      then

       A14: (c . {} ) = {} by A1, A5;

      then

      reconsider T = TopStruct (# X, ( COMPLEMENT ( rng c)) #) as strict TopSpace by A12, A8, A9, Th7;

      take T;

      thus the carrier of T = X;

      let A be Subset of T;

      

      thus ( Cl A) = (c . A) by A14, A8, A9, A12, Th7

      .= ClOp(A) by A5;

    end;

    theorem :: TOPGEN_3:8

    

     Th8: for T1,T2 be TopSpace st the carrier of T1 = the carrier of T2 & for A1 be Subset of T1, A2 be Subset of T2 st A1 = A2 holds ( Cl A1) = ( Cl A2) holds the topology of T1 = the topology of T2

    proof

      let T1,T2 be TopSpace such that

       A1: the carrier of T1 = the carrier of T2 and

       A2: for A1 be Subset of T1, A2 be Subset of T2 st A1 = A2 holds ( Cl A1) = ( Cl A2);

      now

        let A be set;

        thus A is closed Subset of T1 implies A is closed Subset of T2

        proof

          assume A is closed Subset of T1;

          then

          reconsider A1 = A as closed Subset of T1;

          reconsider A2 = A1 as Subset of T2 by A1;

          ( Cl A1) = A1 by PRE_TOPC: 22;

          then ( Cl A2) = A2 by A2;

          hence thesis;

        end;

        assume A is closed Subset of T2;

        then

        reconsider A2 = A as closed Subset of T2;

        reconsider A1 = A2 as Subset of T1 by A1;

        ( Cl A2) = A2 by PRE_TOPC: 22;

        then ( Cl A1) = A1 by A2;

        hence A is closed Subset of T1;

      end;

      then the TopStruct of T1 = the TopStruct of T2 by Th6;

      hence thesis;

    end;

    theorem :: TOPGEN_3:9

    

     Th9: for X be set, i be Function of ( bool X), ( bool X) st (i . X) = X & (for A be Subset of X holds (i . A) c= A) & (for A,B be Subset of X holds (i . (A /\ B)) = ((i . A) /\ (i . B))) & (for A be Subset of X holds (i . (i . A)) = (i . A)) holds for T be TopStruct st the carrier of T = X & the topology of T = ( rng i) holds T is TopSpace & for A be Subset of T holds ( Int A) = (i . A)

    proof

      let X be set;

      let c be Function of ( bool X), ( bool X) such that

       A1: (c . X) = X and

       A2: for A be Subset of X holds (c . A) c= A and

       A3: for A,B be Subset of X holds (c . (A /\ B)) = ((c . A) /\ (c . B)) and

       A4: for A be Subset of X holds (c . (c . A)) = (c . A);

      set F = ( rng c);

      let T be TopStruct such that

       A5: the carrier of T = X and

       A6: the topology of T = ( rng c);

      

       A7: ( dom c) = ( bool X) by FUNCT_2:def 1;

       A8:

      now

        let A,B be Subset of T;

        assume that

         A9: A in F and

         A10: B in F;

        consider a be object such that

         A11: a in ( dom c) and

         A12: A = (c . a) by A9, FUNCT_1:def 3;

        consider b be object such that

         A13: b in ( dom c) and

         A14: B = (c . b) by A10, FUNCT_1:def 3;

        reconsider a, b as Subset of X by A11, A13;

        (A /\ B) = ((c . A) /\ B) by A4, A11, A12

        .= ((c . A) /\ (c . B)) by A4, A13, A14

        .= (c . ((c . a) /\ (c . b))) by A3, A12, A14;

        hence (A /\ B) in F by A7, FUNCT_1:def 3;

      end;

       A15:

      now

        let A,B be Subset of X;

        assume A c= B;

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

        then (c . A) = ((c . A) /\ (c . B)) by A3;

        hence (c . A) c= (c . B) by XBOOLE_1: 17;

      end;

       A16:

      now

        let G be Subset-Family of X such that

         A17: G c= F;

        now

          let a;

          assume

           A18: a in G;

          then

          reconsider A = a as Subset of X;

          

           A19: (c . A) c= (c . ( union G)) by A15, A18, ZFMISC_1: 74;

          ex b be object st b in ( dom c) & A = (c . b) by A17, A18, FUNCT_1:def 3;

          hence a c= (c . ( union G)) by A19, A4;

        end;

        then

         A20: ( union G) c= (c . ( union G)) by ZFMISC_1: 76;

        (c . ( union G)) c= ( union G) by A2;

        then (c . ( union G)) = ( union G) by A20;

        hence ( union G) in F by A7, FUNCT_1:def 3;

      end;

      X in F by A1, A7, FUNCT_1:def 3;

      hence

       A21: T is TopSpace by A16, A5, A6, A8, PRE_TOPC:def 1;

      let A be Subset of T;

      reconsider B = A, IntA = ( Int A) as Subset of X by A5;

      IntA in F by A21, A6, PRE_TOPC:def 2;

      then ex a be object st a in ( dom c) & IntA = (c . a) by FUNCT_1:def 3;

      then (c . IntA) = IntA by A4;

      hence ( Int A) c= (c . A) by A5, A15, TOPS_1: 16;

      reconsider cB = (c . B) as Subset of T by A5;

      cB in F by A7, FUNCT_1:def 3;

      then cB is open by A6;

      hence thesis by A2, TOPS_1: 24;

    end;

    scheme :: TOPGEN_3:sch3

    TopDefByInteriorOp { X() -> set , IntOp( object) -> set } :

ex T be strict TopSpace st the carrier of T = X() & for A be Subset of T holds ( Int A) = IntOp(A)

      provided

       A1: IntOp(X) = X()

       and

       A2: for A be Subset of X() holds IntOp(A) c= A

       and

       A3: for A,B be Subset of X() holds IntOp(/\) = (IntOp(A) /\ IntOp(B))

       and

       A4: for A be Subset of X() holds IntOp(IntOp) = IntOp(A);

      set X = X();

      consider c be Function such that

       A5: ( dom c) = ( bool X) & for a st a in ( bool X) holds (c . a) = IntOp(a) from FUNCT_1:sch 5;

      now

        let a be object;

        assume

         A6: a in ( bool X);

        reconsider aa = a as set by TARSKI: 1;

        

         A7: IntOp(a) c= aa by A2, A6;

        (c . a) = IntOp(a) by A6, A5;

        then (c . a) c= X by A7, A6, XBOOLE_1: 1;

        hence (c . a) in ( bool X);

      end;

      then

      reconsider c as Function of ( bool X), ( bool X) by A5, FUNCT_2: 3;

      

       A8: for A be Subset of X holds (c . A) c= A

      proof

        let A be Subset of X;

        (c . A) = IntOp(A) by A5;

        hence thesis by A2;

      end;

      

       A9: for A,B be Subset of X holds (c . (A /\ B)) = ((c . A) /\ (c . B))

      proof

        let A,B be Subset of X;

        

         A10: (c . B) = IntOp(B) by A5;

        

         A11: IntOp(/\) = (c . (A /\ B)) by A5;

        (c . A) = IntOp(A) by A5;

        hence thesis by A10, A11, A3;

      end;

      

       A12: for A be Subset of X holds (c . (c . A)) = (c . A)

      proof

        let A be Subset of X;

        

         A13: IntOp(.) = (c . (c . A)) by A5;

        (c . A) = IntOp(A) by A5;

        hence thesis by A13, A4;

      end;

      

       A14: (c . X) = X by A1, A5;

      then

      reconsider T = TopStruct (# X, ( rng c) #) as strict TopSpace by A12, A8, A9, Th9;

      take T;

      thus the carrier of T = X;

      let A be Subset of T;

      

      thus ( Int A) = (c . A) by A14, A8, A9, A12, Th9

      .= IntOp(A) by A5;

    end;

    theorem :: TOPGEN_3:10

    

     Th10: for T1,T2 be TopSpace st the carrier of T1 = the carrier of T2 & for A1 be Subset of T1, A2 be Subset of T2 st A1 = A2 holds ( Int A1) = ( Int A2) holds the topology of T1 = the topology of T2

    proof

      let T1,T2 be TopSpace such that

       A1: the carrier of T1 = the carrier of T2 and

       A2: for A1 be Subset of T1, A2 be Subset of T2 st A1 = A2 holds ( Int A1) = ( Int A2);

      now

        let A1 be Subset of T1, A2 be Subset of T2;

        assume A1 = A2;

        then ( Int (A1 ` )) = ( Int (A2 ` )) by A1, A2;

        

        hence ( Cl A1) = (( Int (A2 ` )) ` ) by A1, TDLAT_3: 1

        .= ( Cl A2) by TDLAT_3: 1;

      end;

      hence thesis by A1, Th8;

    end;

    begin

    definition

      ::$Notion-Name

      :: TOPGEN_3:def2

      func Sorgenfrey-line -> strict non empty TopSpace means

      : Def2: the carrier of it = REAL & ex B be Subset-Family of REAL st the topology of it = ( UniCl B) & B = { [.x, q.[ where x,q be Real : x < q & q is rational };

      uniqueness ;

      existence

      proof

        set B = { [.x, q.[ where x,q be Real : x < q & q is rational };

        B c= ( bool REAL )

        proof

          let a be object;

          assume a in B;

          then ex x,q be Real st a = [.x, q.[ & x < q & q is rational;

          hence thesis;

        end;

        then

        reconsider B as Subset-Family of REAL ;

        

         A1: B is point-filtered

        proof

          let x,U1,U2 be set such that

           A2: U1 in B and

           A3: U2 in B and

           A4: x in (U1 /\ U2);

          consider x1,q1 be Real such that

           A5: U1 = [.x1, q1.[ and

           A6: x1 < q1 and

           A7: q1 is rational by A2;

          consider x2,q2 be Real such that

           A8: U2 = [.x2, q2.[ and

           A9: x2 < q2 and

           A10: q2 is rational by A3;

          set y = ( max (x1,x2)), q = ( min (q1,q2));

          

           A11: q is rational by A7, A10, XXREAL_0: 15;

          

           A12: x in U1 by A4, XBOOLE_0:def 4;

          then

          reconsider x9 = x as Element of REAL by A5;

          

           A13: x in U2 by A4, XBOOLE_0:def 4;

          then

           A14: x2 <= x9 by A8, XXREAL_1: 3;

          

           A15: x9 < q2 by A8, A13, XXREAL_1: 3;

          

           A16: q <= q2 by XXREAL_0: 17;

          x2 <= y by XXREAL_0: 31;

          then

           A17: [.y, q.[ c= U2 by A16, A8, XXREAL_1: 38;

          

           A18: q <= q1 by XXREAL_0: 17;

          x1 <= y by XXREAL_0: 31;

          then

           A19: [.y, q.[ c= U1 by A18, A5, XXREAL_1: 38;

          

           A20: x1 <= x9 by A5, A12, XXREAL_1: 3;

          then x1 < q2 by A15, XXREAL_0: 2;

          then

           A21: y < q2 by A9, XXREAL_0: 29;

          

           A22: x9 < q1 by A5, A12, XXREAL_1: 3;

          then

           A23: x9 < q by A15, XXREAL_0: 15;

          x2 < q1 by A14, A22, XXREAL_0: 2;

          then y < q1 by A6, XXREAL_0: 29;

          then y < q by A21, XXREAL_0: 15;

          then

           A24: [.y, q.[ in B by A11;

          y <= x9 by A20, A14, XXREAL_0: 28;

          then x9 in [.y, q.[ by A23, XXREAL_1: 3;

          hence thesis by A24, A19, A17, XBOOLE_1: 19;

        end;

        now

          let x be set;

          assume x in REAL ;

          then

          reconsider x9 = x as Element of REAL ;

          (x9 + 0 ) < (x9 + 1) by XREAL_1: 6;

          then

          consider q be Rational such that

           A25: x9 < q and q < (x9 + 1) by RAT_1: 7;

          take U = [.x9, q.[;

          thus U in B by A25;

          thus x in U by A25, XXREAL_1: 3;

        end;

        then B is covering by Th1;

        then TopStruct (# REAL , ( UniCl B) #) is non empty TopSpace by A1, Th2;

        hence thesis;

      end;

    end

    

     Lm3: the carrier of Sorgenfrey-line = REAL by Def2;

    consider BB be Subset-Family of REAL such that

     Lm4: the topology of Sorgenfrey-line = ( UniCl BB) and

     Lm5: BB = { [.x, q.[ where x,q be Real : x < q & q is rational } by Def2;

    BB c= the topology of Sorgenfrey-line by Lm4, CANTOR_1: 1;

    then

     Lm6: BB is Basis of Sorgenfrey-line by Lm3, Lm4, CANTOR_1:def 2, TOPS_2: 64;

    theorem :: TOPGEN_3:11

    

     Th11: for x,y be Real holds [.x, y.[ is open Subset of Sorgenfrey-line

    proof

      let x,y be Real;

      reconsider V = [.x, y.[ as Subset of Sorgenfrey-line by Def2;

      now

        let p be Point of Sorgenfrey-line ;

        reconsider a = p as Element of REAL by Def2;

        assume

         A1: p in [.x, y.[;

        then

         A2: x <= a by XXREAL_1: 3;

        a < y by A1, XXREAL_1: 3;

        then

        consider q be Rational such that

         A3: a < q and

         A4: q < y by RAT_1: 7;

        reconsider U = [.x, q.[ as Subset of Sorgenfrey-line by Def2;

        take U;

        x < q by A2, A3, XXREAL_0: 2;

        hence U in BB by Lm5;

        thus p in U by A2, A3, XXREAL_1: 3;

        thus U c= V by A4, XXREAL_1: 38;

      end;

      hence thesis by Lm6, YELLOW_9: 31;

    end;

    theorem :: TOPGEN_3:12

    for x,y be Real holds ].x, y.[ is open Subset of Sorgenfrey-line

    proof

      let x,y be Real;

      reconsider V = ].x, y.[ as Subset of Sorgenfrey-line by Def2;

      now

        let p be Point of Sorgenfrey-line ;

        reconsider a = p as Element of REAL by Def2;

        assume

         A1: p in V;

        then a < y by XXREAL_1: 4;

        then

        consider q be Rational such that

         A2: a < q and

         A3: q < y by RAT_1: 7;

        reconsider U = [.a, q.[ as Subset of Sorgenfrey-line by Def2;

        take U;

        thus U in BB by A2, Lm5;

        thus p in U by A2, XXREAL_1: 3;

        x < a by A1, XXREAL_1: 4;

        hence U c= V by A3, XXREAL_1: 48;

      end;

      hence thesis by Lm6, YELLOW_9: 31;

    end;

    theorem :: TOPGEN_3:13

    for x be Real holds ( left_open_halfline x) is open Subset of Sorgenfrey-line

    proof

      let x be Real;

      reconsider V = ( left_open_halfline x) as Subset of Sorgenfrey-line by Def2;

      now

        let p be Point of Sorgenfrey-line ;

        reconsider a = p as Element of REAL by Def2;

        assume

         A1: p in V;

        then

         A2: {a} c= V by ZFMISC_1: 31;

        a < x by A1, XXREAL_1: 233;

        then

        consider q be Rational such that

         A3: a < q and

         A4: q < x by RAT_1: 7;

        reconsider U = [.a, q.[ as Subset of Sorgenfrey-line by Def2;

        take U;

        thus U in BB by A3, Lm5;

        thus p in U by A3, XXREAL_1: 3;

        

         A5: ].a, q.[ c= V by A4, XXREAL_1: 263;

        U = ( {a} \/ ].a, q.[) by A3, XXREAL_1: 131;

        hence U c= V by A2, A5, XBOOLE_1: 8;

      end;

      hence thesis by Lm6, YELLOW_9: 31;

    end;

    theorem :: TOPGEN_3:14

    for x be Real holds ( right_open_halfline x) is open Subset of Sorgenfrey-line

    proof

      let x be Real;

      reconsider V = ( right_open_halfline x) as Subset of Sorgenfrey-line by Def2;

      now

        let p be Point of Sorgenfrey-line ;

        reconsider a = p as Element of REAL by Def2;

        assume

         A1: p in V;

        then

         A2: {a} c= V by ZFMISC_1: 31;

        (a + 0 ) < (a + 1) by XREAL_1: 6;

        then

        consider q be Rational such that

         A3: a < q and q < (a + 1) by RAT_1: 7;

        reconsider U = [.a, q.[ as Subset of Sorgenfrey-line by Def2;

        take U;

        thus U in BB by A3, Lm5;

        thus p in U by A3, XXREAL_1: 3;

        a > x by A1, XXREAL_1: 235;

        then

         A4: ].a, q.[ c= V by XXREAL_1: 247;

        U = ( {a} \/ ].a, q.[) by A3, XXREAL_1: 131;

        hence U c= V by A2, A4, XBOOLE_1: 8;

      end;

      hence thesis by Lm6, YELLOW_9: 31;

    end;

    theorem :: TOPGEN_3:15

    for x be Real holds ( right_closed_halfline x) is open Subset of Sorgenfrey-line

    proof

      let x be Real;

      reconsider V = ( right_closed_halfline x) as Subset of Sorgenfrey-line by Def2;

      now

        let p be Point of Sorgenfrey-line ;

        reconsider a = p as Element of REAL by Def2;

        (a + 0 ) < (a + 1) by XREAL_1: 6;

        then

        consider q be Rational such that

         A1: a < q and q < (a + 1) by RAT_1: 7;

        a in [.a, q.] by A1, XXREAL_1: 1;

        then

         A2: {a} c= [.a, q.] by ZFMISC_1: 31;

        reconsider U = [.a, q.[ as Subset of Sorgenfrey-line by Def2;

        assume p in V;

        then a >= x by XXREAL_1: 236;

        then

         A3: [.a, q.] c= V by XXREAL_1: 251;

        take U;

        thus U in BB by A1, Lm5;

        thus p in U by A1, XXREAL_1: 3;

        

         A4: ].a, q.[ c= [.a, q.] by XXREAL_1: 37;

        U = ( {a} \/ ].a, q.[) by A1, XXREAL_1: 131;

        then U c= [.a, q.] by A2, A4, XBOOLE_1: 8;

        hence U c= V by A3;

      end;

      hence thesis by Lm6, YELLOW_9: 31;

    end;

    theorem :: TOPGEN_3:16

    

     Th16: ( card INT ) = omega

    proof

      

       A1: ( card INT ) c= ( card ( NAT \/ [: { 0 }, NAT :])) by CARD_1: 11, NUMBERS:def 4;

      

       A2: ( card [: NAT , { 0 }:]) = ( card [: { 0 }, NAT :]) by CARD_2: 4;

      

       A3: ( card [: NAT , { 0 }:]) = ( card NAT ) by CARD_1: 69;

      ( omega +` omega qua cardinal number) = omega by CARD_2: 75;

      then ( card ( NAT \/ [: { 0 }, NAT :])) c= omega by A3, A2, CARD_2: 34;

      hence ( card INT ) c= omega by A1;

      thus thesis by CARD_1: 11, CARD_1: 47, NUMBERS: 17;

    end;

    ::$Notion-Name

    theorem :: TOPGEN_3:17

    

     Th17: ( card RAT ) = omega

    proof

      defpred P[ object, object] means ex i be Integer, n be Nat st $1 = [i, n] & $2 = (i / n);

      

       A1: for a be object st a in [: INT , NAT :] holds ex b be object st P[a, b]

      proof

        let a be object;

        assume a in [: INT , NAT :];

        then

        consider x,y be object such that

         A2: x in INT and

         A3: y in NAT and

         A4: a = [x, y] by ZFMISC_1:def 2;

        reconsider y as Nat by A3;

        reconsider x as Integer by A2;

        (x / y) = (x / y);

        hence thesis by A4;

      end;

      consider f be Function such that

       A5: ( dom f) = [: INT , NAT :] & for a be object st a in [: INT , NAT :] holds P[a, (f . a)] from CLASSES1:sch 1( A1);

      

       A6: RAT c= ( rng f)

      proof

        let a be object;

        assume a in RAT ;

        then

        consider i,j be Integer such that

         A7: a = (i / j) by RAT_1:def 1;

        consider n be Nat such that

         A8: j = n or j = ( - n) by INT_1: 2;

        (i / ( - n)) = ( - (i / n)) by XCMPLX_1: 188;

        then a = (i / n) or a = (( - i) / n) by A7, A8, XCMPLX_1: 187;

        then

        consider k be Integer such that

         A9: a = (k / n);

        k in INT & n in NAT by INT_1:def 2, ORDINAL1:def 12;

        then

         A10: [k, n] in [: INT , NAT :] by ZFMISC_1:def 2;

        then

        consider i1 be Integer, n1 be Nat such that

         A11: [k, n] = [i1, n1] and

         A12: (f . [k, n]) = (i1 / n1) by A5;

        

         A13: n = n1 by A11, XTUPLE_0: 1;

        i1 = k by A11, XTUPLE_0: 1;

        hence thesis by A13, A5, A9, A10, A12, FUNCT_1:def 3;

      end;

      ( card [: INT , NAT :]) = ( card [: omega , omega :]) by Th16, CARD_2: 7

      .= omega by CARD_2:def 2, CARD_4: 6;

      hence ( card RAT ) c= omega by A5, A6, CARD_1: 12;

      thus omega c= ( card RAT ) by CARD_1: 11, CARD_1: 47, NUMBERS: 18;

    end;

    theorem :: TOPGEN_3:18

    

     Th18: for A be set st A is mutually-disjoint & for a st a in A holds ex x,y be Real st x < y & ].x, y.[ c= a holds A is countable

    proof

      defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 in D1;

      let A be set such that

       A1: for a, b st a in A & b in A & a <> b holds a misses b;

      assume

       A2: a in A implies ex x,y be Real st x < y & ].x, y.[ c= a;

       A3:

      now

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume a in A;

        then

        consider x,y be Real such that

         A4: x < y and

         A5: ].x, y.[ c= aa by A2;

        consider q be Rational such that

         A6: x < q and

         A7: q < y by A4, RAT_1: 7;

        

         A8: q in RAT by RAT_1:def 2;

        q in ].x, y.[ by A6, A7, XXREAL_1: 4;

        hence ex q be object st q in RAT & P[a, q] by A5, A8;

      end;

      consider f be Function such that

       A9: ( dom f) = A & ( rng f) c= RAT and

       A10: for a be object st a in A holds P[a, (f . a)] from FUNCT_1:sch 6( A3);

      f is one-to-one

      proof

        let a,b be object;

        assume that

         A11: a in ( dom f) and

         A12: b in ( dom f) and

         A13: (f . a) = (f . b) and

         A14: a <> b;

        reconsider a, b as set by TARSKI: 1;

         P[b, (f . b)] by A12, A9, A10;

        then

         A15: (f . a) in b by A13;

         P[a, (f . a)] by A11, A9, A10;

        then

         A16: (f . a) in a;

        a misses b by A11, A12, A14, A1, A9;

        hence thesis by A16, A15, XBOOLE_0: 3;

      end;

      then ( card A) c= ( card RAT ) by A9, CARD_1: 10;

      hence thesis by Th17;

    end;

    definition

      let X be set;

      let x be Real;

      :: TOPGEN_3:def3

      pred x is_local_minimum_of X means x in X & ex y be Real st y < x & ].y, x.[ misses X;

    end

    theorem :: TOPGEN_3:19

    

     Th19: for U be Subset of REAL holds { x where x be Element of REAL : x is_local_minimum_of U } is countable

    proof

      let U be Subset of REAL ;

      set X = { x where x be Element of REAL : x is_local_minimum_of U };

      defpred P[ object, object] means ex x,y be Real st $1 = x & $2 = ].y, x.[ & y < x & ].y, x.[ misses U;

       A1:

      now

        let a be object;

        assume a in X;

        then

        consider x be Element of REAL such that

         A2: a = x and

         A3: x is_local_minimum_of U;

        ex y be Real st y < x & ].y, x.[ misses U by A3;

        hence ex b be object st b in ( bool REAL ) & P[a, b] by A2;

      end;

      consider f be Function such that

       A4: ( dom f) = X & ( rng f) c= ( bool REAL ) and

       A5: for a be object st a in X holds P[a, (f . a)] from FUNCT_1:sch 6( A1);

      f is one-to-one

      proof

        let a9,b9 be object;

        set a = (f . a9), b = (f . b9);

        assume that

         A6: a9 in ( dom f) and

         A7: b9 in ( dom f);

        consider xb,yb be Real such that

         A8: b9 = xb and

         A9: b = ].yb, xb.[ and yb < xb and

         A10: ].yb, xb.[ misses U by A4, A5, A7;

        ex x be Element of REAL st xb = x & x is_local_minimum_of U by A4, A7, A8;

        then

         A11: xb in U;

        assume that

         A12: a = b and

         A13: a9 <> b9;

        consider xa,ya be Real such that

         A14: a9 = xa and

         A15: a = ].ya, xa.[ and

         A16: ya < xa and

         A17: ].ya, xa.[ misses U by A4, A5, A6;

        consider c be Rational such that

         A18: ya < c and

         A19: c < xa by A16, RAT_1: 7;

        

         A20: c in a by A15, A18, A19, XXREAL_1: 4;

        then

         A21: c < xb by A9, A12, XXREAL_1: 4;

        ex x be Element of REAL st xa = x & x is_local_minimum_of U by A4, A6, A14;

        then

         A22: xa in U;

        yb < c by A9, A12, A20, XXREAL_1: 4;

        then yb < xa & xa < xb or xa > xb & xb > ya by A19, A18, A21, A14, A8, A13, XXREAL_0: 1, XXREAL_0: 2;

        then xa in b or xb in a by A15, A9, XXREAL_1: 4;

        hence thesis by A15, A17, A9, A10, A11, A22, XBOOLE_0: 3;

      end;

      then

       A23: ( card X) c= ( card ( rng f)) by A4, CARD_1: 10;

      

       A24: ( rng f) is mutually-disjoint

      proof

        let a, b;

        assume a in ( rng f);

        then

        consider a9 be object such that

         A25: a9 in ( dom f) and

         A26: a = (f . a9) by FUNCT_1:def 3;

        consider xa,ya be Real such that

         A27: a9 = xa and

         A28: a = ].ya, xa.[ and ya < xa and

         A29: ].ya, xa.[ misses U by A4, A5, A25, A26;

        ex x be Element of REAL st xa = x & x is_local_minimum_of U by A4, A25, A27;

        then

         A30: xa in U;

        assume b in ( rng f);

        then

        consider b9 be object such that

         A31: b9 in ( dom f) and

         A32: b = (f . b9) by FUNCT_1:def 3;

        consider xb,yb be Real such that

         A33: b9 = xb and

         A34: b = ].yb, xb.[ and yb < xb and

         A35: ].yb, xb.[ misses U by A4, A5, A31, A32;

        assume that

         A36: a <> b and

         A37: a meets b;

        consider c be object such that

         A38: c in a and

         A39: c in b by A37, XBOOLE_0: 3;

        reconsider c as Element of REAL by A28, A38;

        

         A40: c < xa by A28, A38, XXREAL_1: 4;

        ex x be Element of REAL st xb = x & x is_local_minimum_of U by A4, A31, A33;

        then

         A41: xb in U;

        

         A42: c < xb by A34, A39, XXREAL_1: 4;

        

         A43: ya < c by A28, A38, XXREAL_1: 4;

        yb < c by A34, A39, XXREAL_1: 4;

        then yb < xa & xa < xb or xa > xb & xb > ya by A40, A43, A42, A26, A32, A27, A33, A36, XXREAL_0: 1, XXREAL_0: 2;

        then xa in b or xb in a by A28, A34, XXREAL_1: 4;

        hence thesis by A28, A29, A34, A35, A41, A30, XBOOLE_0: 3;

      end;

      now

        let a;

        assume a in ( rng f);

        then

        consider b be object such that

         A44: b in ( dom f) and

         A45: a = (f . b) by FUNCT_1:def 3;

        consider x,y be Real such that b = x and

         A46: a = ].y, x.[ and

         A47: y < x and ].y, x.[ misses U by A4, A5, A44, A45;

        take y, x;

        thus y < x & ].y, x.[ c= a by A46, A47;

      end;

      then ( rng f) is countable by A24, Th18;

      then ( card ( rng f)) c= omega ;

      hence ( card X) c= omega by A23;

    end;

    registration

      let M be Aleph;

      cluster ( exp (2,M)) -> infinite;

      coherence

      proof

        ( card M) = M;

        then ( exp (2,M)) = ( card ( bool M)) by CARD_2: 31;

        hence thesis;

      end;

    end

    definition

      :: TOPGEN_3:def4

      func continuum -> infinite cardinal number equals ( card REAL );

      coherence ;

    end

    theorem :: TOPGEN_3:20

    

     Th20: ( card { [.x, q.[ where x,q be Real : x < q & q is rational }) = continuum

    proof

      defpred P[ object, object] means ex x be Element of REAL , q be Element of REAL st $1 = x & $2 = [.x, q.[ & x < q & q is rational;

      deffunc F( Element of [: REAL , RAT :]) = [.($1 `1 ), ($1 `2 ).[;

      set X = { [.x, q.[ where x,q be Real : x < q & q is rational };

      consider f be Function such that

       A1: ( dom f) = [: REAL , RAT :] and

       A2: for z be Element of [: REAL , RAT :] holds (f . z) = F(z) from FUNCT_1:sch 4;

      

       A3: X c= ( rng f)

      proof

        let a be object;

        assume a in X;

        then

        consider x,q be Real such that

         A4: a = [.x, q.[ and x < q and

         A5: q is rational;

        x in REAL & q in RAT by A5, RAT_1:def 2, XREAL_0:def 1;

        then

        reconsider b = [x, q] as Element of [: REAL , RAT :] by ZFMISC_1:def 2;

        

         A6: (b `2 ) = q;

        (b `1 ) = x;

        then (f . b) = [.x, q.[ by A6, A2;

        hence thesis by A1, A4, FUNCT_1:def 3;

      end;

      ( card omega ) c= ( card REAL ) by CARD_1: 11, NUMBERS: 19;

      then

       A7: omega c= continuum ;

      ( card [: REAL , RAT :]) = ( card [:( card REAL ), ( card RAT ):]) by CARD_2: 7

      .= ( continuum *` omega ) by Th17, CARD_2:def 2

      .= continuum by A7, CARD_4: 16;

      hence ( card X) c= continuum by A1, A3, CARD_1: 12;

      

       A8: for a be object st a in REAL holds ex b be object st b in X & P[a, b]

      proof

        let a be object;

        assume a in REAL ;

        then

        reconsider x = a as Element of REAL ;

        (x + 0 ) < (x + 1) by XREAL_1: 6;

        then

        consider q be Rational such that

         A9: x < q and q < (x + 1) by RAT_1: 7;

        q in RAT by RAT_1:def 2;

        then

        reconsider q as Element of REAL by NUMBERS: 12;

         [.x, q.[ in X by A9;

        hence thesis by A9;

      end;

      consider f be Function such that

       A10: ( dom f) = REAL & ( rng f) c= X & for a be object st a in REAL holds P[a, (f . a)] from FUNCT_1:sch 6( A8);

      f is one-to-one

      proof

        let a,b be object;

        assume a in ( dom f);

        then

        consider x be Element of REAL , q be Element of REAL such that

         A11: a = x and

         A12: (f . a) = [.x, q.[ and

         A13: x < q and q is rational by A10;

        assume b in ( dom f);

        then

        consider y be Element of REAL , r be Element of REAL such that

         A14: b = y and

         A15: (f . b) = [.y, r.[ and

         A16: y < r and r is rational by A10;

        assume

         A17: (f . a) = (f . b);

        then y in [.x, q.[ by A12, A15, A16, XXREAL_1: 3;

        then

         A18: x <= y by XXREAL_1: 3;

        x in [.y, r.[ by A17, A12, A13, A15, XXREAL_1: 3;

        then y <= x by XXREAL_1: 3;

        hence thesis by A18, A11, A14, XXREAL_0: 1;

      end;

      hence thesis by A10, CARD_1: 10;

    end;

    definition

      let X be set, r be Real;

      :: TOPGEN_3:def5

      func X -powers r -> sequence of REAL means

      : Def5: for i be Nat holds i in X & (it . i) = (r |^ i) or not i in X & (it . i) = 0 ;

      existence

      proof

        deffunc G( object) = 0 ;

        deffunc F( object) = (r |^ ( In ($1, NAT )));

        defpred C[ object] means $1 in X;

        

         A1: for a be object st a in NAT holds ( C[a] implies F(a) in REAL ) & ( not C[a] implies G(a) in REAL ) by XREAL_0:def 1;

        consider f be sequence of REAL such that

         A2: for a be object st a in NAT holds ( C[a] implies (f . a) = F(a)) & ( not C[a] implies (f . a) = G(a)) from FUNCT_2:sch 5( A1);

        take f;

        let i be Nat;

        ( In (i, NAT )) = i;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of REAL such that

         A3: for i be Nat holds i in X & (f1 . i) = (r |^ i) or not i in X & (f1 . i) = 0 and

         A4: for i be Nat holds i in X & (f2 . i) = (r |^ i) or not i in X & (f2 . i) = 0 ;

        now

          let i be Element of NAT ;

          i in X & (f1 . i) = (r |^ i) or not i in X & (f1 . i) = 0 by A3;

          hence (f1 . i) = (f2 . i) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: TOPGEN_3:21

    

     Th21: for X be set, r be Real st 0 < r & r < 1 holds (X -powers r) is summable

    proof

      let X be set, r be Real such that

       A1: 0 < r and

       A2: r < 1;

       A3:

      now

        let n be Nat;

        n in X & ((X -powers r) . n) = (r |^ n) or not n in X & ((X -powers r) . n) = 0 by Def5;

        hence 0 <= ((X -powers r) . n) by A1, PREPOWER: 6;

      end;

       A4:

      now

        reconsider m = 1 as Nat;

        take m;

        let n be Nat such that m <= n;

        

         A5: ((r GeoSeq ) . n) = (r |^ n) by PREPOWER:def 1;

        n in X & ((X -powers r) . n) = (r |^ n) or not n in X & ((X -powers r) . n) = 0 by Def5;

        hence ((X -powers r) . n) <= ((r GeoSeq ) . n) by A1, A5, PREPOWER: 6;

      end;

       |.r.| = r by A1, ABSVALUE:def 1;

      then (r GeoSeq ) is summable by A2, SERIES_1: 24;

      hence thesis by A4, A3, SERIES_1: 19;

    end;

    reserve r for Real,

X for set,

n for Element of NAT ;

    theorem :: TOPGEN_3:22

    

     Th22: 0 < r & r < 1 implies ( Sum ((r GeoSeq ) ^\ n)) = ((r |^ n) / (1 - r))

    proof

      assume that

       A1: 0 < r and

       A2: r < 1;

      

       A3: |.r.| = r by A1, ABSVALUE:def 1;

      then

       A4: (r GeoSeq ) is summable by A2, SERIES_1: 24;

      

       A5: ( dom ((r |^ n) (#) (r GeoSeq ))) = NAT by FUNCT_2:def 1;

      now

        let i be Element of NAT ;

        

        thus (((r GeoSeq ) ^\ n) . i) = ((r GeoSeq ) . (i + n)) by NAT_1:def 3

        .= (r |^ (i + n)) by PREPOWER:def 1

        .= ((r |^ n) * (r |^ i)) by NEWTON: 8

        .= ((r |^ n) * ((r GeoSeq ) . i)) by PREPOWER:def 1

        .= (((r |^ n) (#) (r GeoSeq )) . i) by A5, VALUED_1:def 5;

      end;

      then

       A6: ((r GeoSeq ) ^\ n) = ((r |^ n) (#) (r GeoSeq )) by FUNCT_2: 63;

      ( Sum (r GeoSeq )) = (1 / (1 - r)) by A3, A2, SERIES_1: 24;

      

      hence ( Sum ((r GeoSeq ) ^\ n)) = ((r |^ n) * (1 / (1 - r))) by A4, A6, SERIES_1: 10

      .= (((r |^ n) * 1) / (1 - r)) by XCMPLX_1: 74

      .= ((r |^ n) / (1 - r));

    end;

    theorem :: TOPGEN_3:23

    

     Th23: ( Sum (((1 / 2) GeoSeq ) ^\ (n + 1))) = ((1 / 2) |^ n)

    proof

      set r = (1 / 2);

      

      thus ( Sum (((1 / 2) GeoSeq ) ^\ (n + 1))) = ((r |^ (n + 1)) / (1 - r)) by Th22

      .= ((((1 / 2) |^ n) * r) / r) by NEWTON: 6

      .= (r |^ n);

    end;

    theorem :: TOPGEN_3:24

     0 < r & r < 1 implies ( Sum (X -powers r)) <= ( Sum (r GeoSeq ))

    proof

      assume that

       A1: 0 < r and

       A2: r < 1;

       A3:

      now

        let n be Nat;

        

         A4: n in X & ((X -powers r) . n) = (r |^ n) or not n in X & ((X -powers r) . n) = 0 by Def5;

        hence 0 <= ((X -powers r) . n) by A1, PREPOWER: 6;

        ((r GeoSeq ) . n) = (r |^ n) by PREPOWER:def 1;

        hence ((X -powers r) . n) <= ((r GeoSeq ) . n) by A1, A4, PREPOWER: 6;

      end;

       |.r.| = r by A1, ABSVALUE:def 1;

      then (r GeoSeq ) is summable by A2, SERIES_1: 24;

      hence thesis by A3, SERIES_1: 20;

    end;

    theorem :: TOPGEN_3:25

    

     Th25: ( Sum ((X -powers (1 / 2)) ^\ (n + 1))) <= ((1 / 2) |^ n)

    proof

      set r = (1 / 2);

       |.r.| = r by ABSVALUE:def 1;

      then

       A1: ((r GeoSeq ) ^\ (n + 1)) is summable by SERIES_1: 12, SERIES_1: 24;

       A2:

      now

        let m be Nat;

        

         A3: (((X -powers r) ^\ (n + 1)) . m) = ((X -powers r) . (m + (n + 1))) by NAT_1:def 3;

        

         A4: (m + (n + 1)) in X & ((X -powers r) . (m + (n + 1))) = (r |^ (m + (n + 1))) or not (m + (n + 1)) in X & ((X -powers r) . (m + (n + 1))) = 0 by Def5;

        hence 0 <= (((X -powers r) ^\ (n + 1)) . m) by A3, PREPOWER: 6;

        

         A5: ((r GeoSeq ) . (m + (n + 1))) = (r |^ (m + (n + 1))) by PREPOWER:def 1;

        (((r GeoSeq ) ^\ (n + 1)) . m) = ((r GeoSeq ) . (m + (n + 1))) by NAT_1:def 3;

        hence (((X -powers r) ^\ (n + 1)) . m) <= (((r GeoSeq ) ^\ (n + 1)) . m) by A5, A3, A4, PREPOWER: 6;

      end;

      ( Sum (((1 / 2) GeoSeq ) ^\ (n + 1))) = ((1 / 2) |^ n) by Th23;

      hence thesis by A1, A2, SERIES_1: 20;

    end;

    theorem :: TOPGEN_3:26

    

     Th26: for X be infinite Subset of NAT , i be Nat holds (( Partial_Sums (X -powers (1 / 2))) . i) < ( Sum (X -powers (1 / 2)))

    proof

      set r = (1 / 2);

      let X be infinite Subset of NAT ;

      let i be Nat;

      defpred P[ Nat] means (( Partial_Sums (X -powers r)) . i) <= (( Partial_Sums (X -powers r)) . (i + $1));

       not X c= (i + 1);

      then

      consider a be object such that

       A1: a in X and

       A2: not a in (i + 1);

      reconsider a, j = i as Element of NAT by A1, ORDINAL1:def 12;

      

       A3: ((X -powers r) . a) = (r |^ a) by A1, Def5;

       A4:

      now

        let n be Nat;

        n in X & ((X -powers r) . n) = (r |^ n) or not n in X & ((X -powers r) . n) = 0 by Def5;

        hence 0 <= ((X -powers r) . n) by PREPOWER: 6;

      end;

       A5:

      now

        let k be Nat such that

         A6: P[k];

        (i + (k + 1)) = ((i + k) + 1);

        then

         A7: (( Partial_Sums (X -powers r)) . (j + (k + 1))) = ((( Partial_Sums (X -powers r)) . (j + k)) + ((X -powers r) . (j + (k + 1)))) by SERIES_1:def 1;

        ((X -powers r) . (j + (k + 1))) >= 0 by A4;

        then ((( Partial_Sums (X -powers r)) . (j + k)) + 0 ) <= (( Partial_Sums (X -powers r)) . (j + (k + 1))) by A7, XREAL_1: 6;

        hence P[(k + 1)] by A6, XXREAL_0: 2;

      end;

      ( Segm (j + 1)) c= ( Segm a) by A2, ORDINAL1: 16;

      then (j + 1) <= a by NAT_1: 39;

      then

      consider k be Nat such that

       A8: a = ((j + 1) + k) by NAT_1: 10;

      reconsider k as Element of NAT by ORDINAL1:def 12;

      (r |^ a) > 0 by PREPOWER: 6;

      then

       A9: ((( Partial_Sums (X -powers r)) . i) + (r |^ a)) > ((( Partial_Sums (X -powers r)) . i) + 0 ) by XREAL_1: 6;

      

       A10: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A10, A5);

      then

       A11: (( Partial_Sums (X -powers r)) . i) <= (( Partial_Sums (X -powers r)) . (i + k));

      (j + (k + 1)) = ((j + k) + 1);

      then (( Partial_Sums (X -powers r)) . a) = ((( Partial_Sums (X -powers r)) . (j + k)) + (r |^ a)) by A3, A8, SERIES_1:def 1;

      then ((( Partial_Sums (X -powers r)) . i) + (r |^ a)) <= (( Partial_Sums (X -powers r)) . a) by A11, XREAL_1: 6;

      then

       A12: (( Partial_Sums (X -powers r)) . i) < (( Partial_Sums (X -powers r)) . a) by A9, XXREAL_0: 2;

      (( Partial_Sums (X -powers (1 / 2))) . a) <= ( Sum (X -powers (1 / 2))) by Th21, A4, IRRAT_1: 29;

      hence thesis by A12, XXREAL_0: 2;

    end;

    theorem :: TOPGEN_3:27

    

     Th27: for X,Y be infinite Subset of NAT st ( Sum (X -powers (1 / 2))) = ( Sum (Y -powers (1 / 2))) holds X = Y

    proof

      set r = (1 / 2);

      let X,Y be infinite Subset of NAT such that

       A1: ( Sum (X -powers (1 / 2))) = ( Sum (Y -powers (1 / 2))) and

       A2: X <> Y;

      defpred P[ Nat] means not ($1 in X iff $1 in Y);

      ex a be object st not (a in X iff a in Y) by A2, TARSKI: 2;

      then

       A3: ex i be Nat st P[i];

      consider i be Nat such that

       A4: P[i] & for n be Nat st P[n] holds i <= n from NAT_1:sch 5( A3);

      reconsider i as Element of NAT by ORDINAL1:def 12;

      consider A,B be infinite Subset of NAT such that

       A5: A = X & B = Y or A = Y & B = X and

       A6: i in A and

       A7: not i in B by A4;

      

       A8: ((A -powers r) . i) = (r |^ i) by A6, Def5;

      defpred P[ Nat] means $1 < i implies (( Partial_Sums (A -powers r)) . $1) = (( Partial_Sums (B -powers r)) . $1);

       A9:

      now

        let j be Nat;

        assume

         A10: P[j];

        thus P[(j + 1)]

        proof

          

           A11: (j + 1) in B & ((B -powers r) . (j + 1)) = (r |^ (j + 1)) or not (j + 1) in B & ((B -powers r) . (j + 1)) = 0 by Def5;

          

           A12: (j + 1) in A & ((A -powers r) . (j + 1)) = (r |^ (j + 1)) or not (j + 1) in A & ((A -powers r) . (j + 1)) = 0 by Def5;

          assume

           A13: (j + 1) < i;

          

          hence (( Partial_Sums (A -powers r)) . (j + 1)) = ((( Partial_Sums (B -powers r)) . j) + ((A -powers r) . (j + 1))) by A10, NAT_1: 13, SERIES_1:def 1

          .= (( Partial_Sums (B -powers r)) . (j + 1)) by A12, A11, A13, A4, A5, SERIES_1:def 1;

        end;

      end;

      (( Partial_Sums (A -powers r)) . 0 ) = ((A -powers r) . 0 ) by SERIES_1:def 1;

      then

       A14: 0 in A & (( Partial_Sums (A -powers r)) . 0 ) = (r |^ 0 ) or not 0 in A & (( Partial_Sums (A -powers r)) . 0 ) = 0 by Def5;

      

       A15: ((B -powers r) . i) = 0 by A7, Def5;

      

       A16: (( Partial_Sums (B -powers r)) . 0 ) = ((B -powers r) . 0 ) by SERIES_1:def 1;

      then 0 in B & (( Partial_Sums (B -powers r)) . 0 ) = (r |^ 0 ) or not 0 in B & (( Partial_Sums (B -powers r)) . 0 ) = 0 by Def5;

      then

       A17: P[ 0 ] by A14, A4, A5;

      

       A18: for j be Nat holds P[j] from NAT_1:sch 2( A17, A9);

      

       A19: (( Partial_Sums (A -powers r)) . i) = ((( Partial_Sums (B -powers r)) . i) + (r |^ i))

      proof

        per cases by NAT_1: 6;

          suppose i = 0 ;

          hence thesis by A8, A15, A16, SERIES_1:def 1;

        end;

          suppose ex j be Nat st i = (j + 1);

          then

          consider j be Nat such that

           A20: i = (j + 1);

          reconsider j as Element of NAT by ORDINAL1:def 12;

          j < i by A20, NAT_1: 13;

          then (( Partial_Sums (A -powers r)) . j) = (( Partial_Sums (B -powers r)) . j) by A18;

          

          hence (( Partial_Sums (A -powers r)) . i) = (((( Partial_Sums (B -powers r)) . j) + 0 ) + (r |^ i)) by A8, A20, SERIES_1:def 1

          .= ((( Partial_Sums (B -powers r)) . i) + (r |^ i)) by A15, A20, SERIES_1:def 1;

        end;

      end;

      

       A21: (( Partial_Sums (A -powers r)) . i) < ( Sum (A -powers r)) by Th26;

      

       A22: ( Sum ((B -powers r) ^\ (i + 1))) <= (r |^ i) by Th25;

      ( Sum (B -powers r)) = ((( Partial_Sums (B -powers r)) . i) + ( Sum ((B -powers r) ^\ (i + 1)))) by Th21, SERIES_1: 15;

      hence thesis by A19, A1, A5, A21, A22, XREAL_1: 6;

    end;

    theorem :: TOPGEN_3:28

    

     Th28: X is countable implies ( Fin X) is countable

    proof

      defpred P[ object, object] means ex p be FinSequence st $2 = p & $1 = ( rng p);

      

       A1: X = {} & { {} } is countable or X <> {} ;

      

       A2: for a be object st a in ( Fin X) holds ex b be object st b in (X * ) & P[a, b]

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A3: a in ( Fin X);

        then aa is finite by FINSUB_1:def 5;

        then

        consider p be FinSequence such that

         A4: a = ( rng p) by FINSEQ_1: 52;

        aa c= X by A3, FINSUB_1:def 5;

        then p is FinSequence of X by A4, FINSEQ_1:def 4;

        then p in (X * ) by FINSEQ_1:def 11;

        hence thesis by A4;

      end;

      consider f be Function such that

       A5: ( dom f) = ( Fin X) & ( rng f) c= (X * ) and

       A6: for a be object st a in ( Fin X) holds P[a, (f . a)] from FUNCT_1:sch 6( A2);

      f is one-to-one

      proof

        let a,b be object;

        assume that

         A7: a in ( dom f) and

         A8: b in ( dom f);

        

         A9: P[b, (f . b)] by A8, A5, A6;

         P[a, (f . a)] by A7, A5, A6;

        hence thesis by A9;

      end;

      then

       A10: ( card ( Fin X)) c= ( card (X * )) by A5, CARD_1: 10;

      assume X is countable;

      then (X * ) is countable by A1, CARD_4: 13, FUNCT_7: 17;

      then ( card (X * )) c= omega ;

      hence ( card ( Fin X)) c= omega by A10;

    end;

    theorem :: TOPGEN_3:29

    

     Th29: continuum = ( exp (2, omega ))

    proof

       not [ 0 , 0 ] in RAT+ by ARYTM_3: 33;

      then

       A1: RAT = ( RAT+ \/ ( [: { 0 }, RAT+ :] \ { [ 0 , 0 ]})) by NUMBERS:def 3, XBOOLE_1: 87, ZFMISC_1: 50;

      then ( bool RAT+ ) c= ( bool RAT ) by XBOOLE_1: 7, ZFMISC_1: 67;

      then

       A2: DEDEKIND_CUTS c= ( bool RAT );

       RAT+ c= RAT by A1, XBOOLE_1: 7;

      then ( RAT+ \/ DEDEKIND_CUTS ) c= ( RAT \/ ( bool RAT )) by A2, XBOOLE_1: 13;

      then REAL+ c= ( RAT \/ ( bool RAT )) by ARYTM_2:def 2;

      then

       A3: ( card REAL+ ) c= ( card ( RAT \/ ( bool RAT ))) by CARD_1: 11;

      set INFNAT = (( bool NAT ) \ ( Fin NAT ));

      

       A4: ( card RAT ) in ( card ( bool RAT )) by CARD_1: 14;

      ( card ( RAT \/ ( bool RAT ))) c= (( card RAT ) +` ( card ( bool RAT ))) by CARD_2: 34;

      then ( card REAL+ ) c= (( card RAT ) +` ( card ( bool RAT ))) by A3;

      then ( card REAL+ ) c= ( card ( bool RAT )) by A4, CARD_2: 76;

      then ( card REAL+ ) c= ( exp (2, omega )) by Th17, CARD_2: 31;

      then (( card REAL+ ) +` ( card REAL+ )) c= (( exp (2, omega )) +` ( exp (2, omega ))) by CARD_2: 83;

      then

       A5: (( card REAL+ ) +` ( card REAL+ )) c= ( exp (2, omega )) by CARD_2: 76;

      deffunc F( set) = ( In (( Sum ($1 -powers (1 / 2))), REAL ));

      

       A6: ( card [: { 0 }, REAL+ :]) = ( card [: REAL+ , { 0 }:]) by CARD_2: 4

      .= ( card REAL+ ) by CARD_1: 69;

      

       A7: continuum c= ( card ( REAL+ \/ [: { 0 }, REAL+ :])) by CARD_1: 11, NUMBERS:def 1;

      ( card ( REAL+ \/ [: { 0 }, REAL+ :])) c= (( card REAL+ ) +` ( card [: { 0 }, REAL+ :])) by CARD_2: 34;

      then continuum c= (( card REAL+ ) +` ( card REAL+ )) by A7, A6;

      hence continuum c= ( exp (2, omega )) by A5;

      ( Fin NAT ) is countable by Th28, CARD_4: 2;

      then

       A8: ( card ( Fin NAT )) c= omega ;

      then ( card ( Fin NAT )) in ( card ( bool NAT )) by CARD_1: 14, CARD_1: 47, ORDINAL1: 12;

      then

       A9: (( card ( bool NAT )) +` ( card ( Fin NAT ))) = ( card ( bool NAT )) by CARD_2: 76;

      

       A10: omega in ( card ( bool NAT )) by CARD_1: 14, CARD_1: 47;

      then

      reconsider INFNAT as non empty set by A8, CARD_1: 68, ORDINAL1: 12;

      consider f be Function of INFNAT, REAL such that

       A11: for X be Element of INFNAT holds (f . X) = F(X) from FUNCT_2:sch 4;

      

       A12: f is one-to-one

      proof

        let a,b be object;

        assume that

         A13: a in ( dom f) and

         A14: b in ( dom f);

        reconsider a, b as set by TARSKI: 1;

        

         A15: (f . b) = F(b) by A11, A14;

         not b in ( Fin NAT ) by A14, XBOOLE_0:def 5;

        then

         A16: b is infinite Subset of NAT by A14, FINSUB_1:def 5, XBOOLE_0:def 5;

         not a in ( Fin NAT ) by A13, XBOOLE_0:def 5;

        then

         A17: a is infinite Subset of NAT by A13, FINSUB_1:def 5, XBOOLE_0:def 5;

        (f . a) = F(a) by A11, A13;

        hence thesis by A17, A16, A15, Th27;

      end;

      

       A18: ( rng f) c= REAL by RELAT_1:def 19;

      ( dom f) = INFNAT by FUNCT_2:def 1;

      then ( card INFNAT) c= continuum by A12, A18, CARD_1: 10;

      then ( card ( bool NAT )) c= continuum by A9, A8, A10, CARD_2: 98, ORDINAL1: 12;

      hence thesis by CARD_1: 47, CARD_2: 31;

    end;

    ::$Notion-Name

    theorem :: TOPGEN_3:30

    

     Th30: omega in continuum

    proof

      ( card omega ) in ( card ( bool omega )) by CARD_1: 14;

      hence thesis by Th29, CARD_2: 31;

    end;

    theorem :: TOPGEN_3:31

    

     Th31: for A be Subset-Family of REAL st ( card A) in continuum holds ( card { x where x be Element of REAL : ex U be set st U in ( UniCl A) & x is_local_minimum_of U }) in continuum

    proof

      deffunc F( set) = { x where x be Element of REAL : x is_local_minimum_of $1 };

      let A be Subset-Family of REAL such that

       A1: ( card A) in continuum ;

       A2:

      now

        per cases ;

          suppose ( card A) is empty;

          then (( card A) *` omega ) = 0 by CARD_2: 20;

          hence (( card A) *` omega ) in continuum by ORDINAL3: 8;

        end;

          suppose

           A3: ( card A) is non empty finite;

          then

           A4: ( card ( card A)) in omega by CARD_3: 84;

           0 in ( card A) by A3, ORDINAL3: 8;

          hence (( card A) *` omega ) in continuum by A4, Th30, CARD_4: 16;

        end;

          suppose

           A5: ( card A) is infinite;

          then omega c= ( card A) by CARD_5: 16;

          hence (( card A) *` omega ) in continuum by A1, A5, CARD_4: 16;

        end;

      end;

      set Y = { x where x be Element of REAL : ex U be set st U in A & x is_local_minimum_of U };

      set X = { x where x be Element of REAL : ex U be set st U in ( UniCl A) & x is_local_minimum_of U };

      

       A6: for a be set st a in A holds F(a) in ( bool REAL )

      proof

        let a be set;

         F(a) c= REAL

        proof

          let b be object;

          assume b in F(a);

          then ex x be Element of REAL st b = x & x is_local_minimum_of a;

          hence thesis;

        end;

        hence thesis;

      end;

      consider f be Function of A, ( bool REAL ) such that

       A7: for a be set st a in A holds (f . a) = F(a) from FUNCT_2:sch 11( A6);

      

       A8: X c= Y

      proof

        let a be object;

        assume a in X;

        then

        consider x be Element of REAL such that

         A9: a = x and

         A10: ex U be set st U in ( UniCl A) & x is_local_minimum_of U;

        consider U be set such that

         A11: U in ( UniCl A) and

         A12: x is_local_minimum_of U by A10;

        reconsider U as Subset of REAL by A11;

        consider B be Subset-Family of REAL such that

         A13: B c= A and

         A14: U = ( union B) by A11, CANTOR_1:def 1;

        x in U by A12;

        then

        consider C be set such that

         A15: x in C and

         A16: C in B by A14, TARSKI:def 4;

        consider y be Real such that

         A17: y < x and

         A18: ].y, x.[ misses U by A12;

        reconsider C as Subset of REAL by A16;

         ].y, x.[ misses C

        proof

          assume not thesis;

          then

          consider b be object such that

           A19: b in ].y, x.[ and

           A20: b in C by XBOOLE_0: 3;

          b in U by A14, A16, A20, TARSKI:def 4;

          hence thesis by A18, A19, XBOOLE_0: 3;

        end;

        then x is_local_minimum_of C by A17, A15;

        hence thesis by A13, A16, A9;

      end;

      Y c= ( Union f)

      proof

        let a be object;

        

         A21: ( dom f) = A by FUNCT_2:def 1;

        assume a in Y;

        then

        consider x be Element of REAL such that

         A22: a = x and

         A23: ex U be set st U in A & x is_local_minimum_of U;

        consider U be set such that

         A24: U in A and

         A25: x is_local_minimum_of U by A23;

        

         A26: (f . U) = F(U) by A7, A24;

        a in F(U) by A22, A25;

        hence thesis by A26, A21, A24, CARD_5: 2;

      end;

      then X c= ( Union f) by A8;

      then

       A27: ( card X) c= ( card ( Union f)) by CARD_1: 11;

      

       A28: for a be object holds a in A implies ( card (f . a)) c= omega

      proof

        let a be object;

        assume

         A29: a in A;

        then

        reconsider b = a as Subset of REAL ;

        (f . a) = F(b) by A7, A29;

        then (f . a) is countable by Th19;

        hence thesis;

      end;

      ( dom f) = A by FUNCT_2:def 1;

      then ( card ( Union f)) c= (( card A) *` omega ) by A28, CARD_2: 86;

      hence thesis by A27, A2, ORDINAL1: 12, XBOOLE_1: 1;

    end;

    theorem :: TOPGEN_3:32

    

     Th32: for X be Subset-Family of REAL st ( card X) in continuum holds ex x be Real, q be Rational st x < q & not [.x, q.[ in ( UniCl X)

    proof

      let X be Subset-Family of REAL such that

       A1: ( card X) in continuum ;

      set Z = { x where x be Element of REAL : ex U be set st U in ( UniCl X) & x is_local_minimum_of U };

      set z = the Element of ( REAL \ Z);

      ( card Z) in continuum by A1, Th31;

      then

       A2: ( REAL \ Z) <> {} by CARD_1: 68;

      then

       A3: not z in Z by XBOOLE_0:def 5;

      reconsider z as Element of REAL by A2, XBOOLE_0:def 5;

      (z + 0 ) < (z + 1) by XREAL_1: 6;

      then

      consider q be Rational such that

       A4: z < q and q < (z + 1) by RAT_1: 7;

      take z, q;

      thus z < q by A4;

      z is_local_minimum_of [.z, q.[

      proof

        thus z in [.z, q.[ by A4, XXREAL_1: 3;

        take y = (z - 1);

        (z - 0 ) = z;

        hence y < z by XREAL_1: 15;

        assume ].y, z.[ meets [.z, q.[;

        then

        consider a be object such that

         A5: a in ].y, z.[ and

         A6: a in [.z, q.[ by XBOOLE_0: 3;

        reconsider a as Element of REAL by A5;

        a < z by A5, XXREAL_1: 4;

        hence thesis by A6, XXREAL_1: 3;

      end;

      hence thesis by A3;

    end;

    theorem :: TOPGEN_3:33

    ( weight Sorgenfrey-line ) = continuum

    proof

      thus ( weight Sorgenfrey-line ) c= continuum by Lm5, Lm6, Th20, WAYBEL23: 73;

      consider B be Basis of Sorgenfrey-line such that

       A1: ( weight Sorgenfrey-line ) = ( card B) by WAYBEL23: 74;

      assume not continuum c= ( weight Sorgenfrey-line );

      then

       A2: ( weight Sorgenfrey-line ) in continuum by CARD_1: 4;

      the carrier of Sorgenfrey-line = REAL by Def2;

      then

      consider x be Real, q be Rational such that x < q and

       A3: not [.x, q.[ in ( UniCl B) by A2, A1, Th32;

       [.x, q.[ is open Subset of Sorgenfrey-line by Th11;

      then [.x, q.[ in the topology of Sorgenfrey-line by PRE_TOPC:def 2;

      hence thesis by A3, YELLOW_9: 22;

    end;

    begin

    definition

      let X be set;

      :: TOPGEN_3:def6

      func ClFinTop (X) -> strict TopSpace means

      : Def6: the carrier of it = X & for F be Subset of it holds F is closed iff F is finite or F = X;

      existence

      proof

        defpred C[ set] means $1 c= X & $1 is finite or $1 = X;

        

         A1: X c= X;

        

         A2: for A,B be set st C[A] & C[B] holds C[(A \/ B)]

        proof

          let A,B be set;

          assume that

           A3: C[A] and

           A4: C[B];

          reconsider A, B as Subset of X by A3, A4, A1;

          (A \/ B) c= X;

          hence thesis by A3, A4, XBOOLE_1: 12;

        end;

        

         A5: for G be Subset-Family of X st for A be set st A in G holds C[A] holds C[( Intersect G)]

        proof

          let G be Subset-Family of X;

          assume

           A6: for A be set st A in G holds C[A];

          now

            assume that

             A7: G <> {} and

             A8: G <> {X};

             not G c= {X} by A7, A8, ZFMISC_1: 33;

            then

            consider a be object such that

             A9: a in G and

             A10: not a in {X};

            reconsider aa = a as set by TARSKI: 1;

            

             A11: a <> X by A10, TARSKI:def 1;

             C[aa] by A6, A9;

            hence ( Intersect G) is finite & ( Intersect G) c= X by A11, A9, FINSET_1: 1, MSSUBFAM: 2;

          end;

          hence thesis by A1, MSSUBFAM: 9, SETFAM_1:def 9;

        end;

        

         A12: C[ {} ] & C[X] by XBOOLE_1: 2;

        consider T be strict TopSpace such that

         A13: the carrier of T = X & for A be Subset of T holds A is closed iff C[A] from TopDefByClosedPred( A12, A2, A5);

        take T;

        thus the carrier of T = X by A13;

        let F be Subset of T;

        thus thesis by A13;

      end;

      correctness

      proof

        let T1,T2 be strict TopSpace such that

         A14: the carrier of T1 = X and

         A15: for F be Subset of T1 holds F is closed iff F is finite or F = X and

         A16: the carrier of T2 = X and

         A17: for F be Subset of T2 holds F is closed iff F is finite or F = X;

        now

          let F be set;

          F is closed Subset of T1 iff F c= X & (F is finite or F = X) by A14, A15;

          hence F is closed Subset of T1 iff F is closed Subset of T2 by A16, A17;

        end;

        hence thesis by Th6;

      end;

    end

    theorem :: TOPGEN_3:34

    

     Th34: for X be set, A be Subset of ( ClFinTop X) holds A is open iff A = {} or (A ` ) is finite

    proof

      let X be set, A be Subset of ( ClFinTop X);

      

       A1: the carrier of ( ClFinTop X) = X by Def6;

      hereby

        assume that

         A2: A is open and

         A3: A <> {} ;

        ((A ` ) ` ) = A;

        then (A ` ) <> ( [#] the carrier of ( ClFinTop X)) by A3, XBOOLE_1: 37;

        hence (A ` ) is finite by A2, A1, Def6;

      end;

      assume A = {} or (A ` ) is finite;

      then (A ` ) is closed by Def6;

      hence thesis by TOPS_1: 4;

    end;

    theorem :: TOPGEN_3:35

    

     Th35: for X be infinite set, A be Subset of X st A is finite holds (A ` ) is infinite

    proof

      let X be infinite set, A be Subset of X;

      (A \/ (A ` )) = ( [#] X) by SUBSET_1: 10

      .= X;

      hence thesis;

    end;

    registration

      let X be non empty set;

      cluster ( ClFinTop X) -> non empty;

      coherence by Def6;

    end

    theorem :: TOPGEN_3:36

    for X be infinite set holds for U,V be non empty open Subset of ( ClFinTop X) holds U meets V

    proof

      let X be infinite set;

      let U,V be non empty open Subset of ( ClFinTop X);

      assume U misses V;

      then

       A1: U c= (V ` ) by SUBSET_1: 23;

      

       A2: the carrier of ( ClFinTop X) = X by Def6;

      (V ` ) is finite by Th34;

      then (U ` ) is infinite by A1, A2, Th35;

      then (U ` ) = ( [#] the carrier of ( ClFinTop X)) by A2, Def6;

      then ((U ` ) ` ) = ( {} the carrier of ( ClFinTop X)) by XBOOLE_1: 37;

      hence thesis;

    end;

    begin

    definition

      let X,x0 be set;

      :: TOPGEN_3:def7

      func x0 -PointClTop (X) -> strict TopSpace means

      : Def7: the carrier of it = X & for A be Subset of it holds ( Cl A) = ( IFEQ (A, {} ,A,(A \/ ( {x0} /\ X))));

      existence

      proof

        deffunc ClOp( set) = ( IFEQ ($1, {} ,$1,($1 \/ ( {x0} /\ X))));

        

         A1: for A be Subset of X holds A c= ClOp(A) & ClOp(A) c= X

        proof

          let A be Subset of X;

          A = {} or A <> {} ;

          then

           A2: ClOp(A) = A or ClOp(A) = (A \/ ( {x0} /\ X)) by FUNCOP_1:def 8;

          hence A c= ClOp(A) by XBOOLE_1: 7;

          ( {x0} /\ X) c= X by XBOOLE_1: 17;

          hence thesis by A2, XBOOLE_1: 8;

        end;

        

         A3: ClOp({}) = {} by FUNCOP_1:def 8;

        

         A4: for A,B be Subset of X holds ClOp(\/) = ( ClOp(A) \/ ClOp(B))

        proof

          let A,B be Subset of X;

          per cases ;

            suppose A = {} or B = {} ;

            hence thesis by A3;

          end;

            suppose

             A5: A <> {} & B <> {} ;

            then

             A6: ClOp(\/) = ((A \/ B) \/ ( {x0} /\ X)) by FUNCOP_1:def 8;

            

             A7: ClOp(B) = (B \/ ( {x0} /\ X)) by A5, FUNCOP_1:def 8;

             ClOp(A) = (A \/ ( {x0} /\ X)) by A5, FUNCOP_1:def 8;

            hence thesis by A7, A6, XBOOLE_1: 5;

          end;

        end;

        

         A8: for A be Subset of X holds ClOp(ClOp) = ClOp(A)

        proof

          let A be Subset of X;

          A = {} or A <> {} ;

          then ClOp(A) = {} or (A \/ ( {x0} /\ X)) <> {} & ClOp(A) = (A \/ ( {x0} /\ X)) by FUNCOP_1:def 8;

          then ClOp(ClOp) = ClOp(A) or ClOp(A) = (A \/ ( {x0} /\ X)) & ClOp(ClOp) = ((A \/ ( {x0} /\ X)) \/ ( {x0} /\ X)) by FUNCOP_1:def 8;

          hence thesis by XBOOLE_1: 6;

        end;

        consider T be strict TopSpace such that

         A9: the carrier of T = X & for A be Subset of T holds ( Cl A) = ClOp(A) from TopDefByClosureOp( A3, A1, A4, A8);

        take T;

        thus the carrier of T = X by A9;

        let F be Subset of T;

        thus thesis by A9;

      end;

      correctness

      proof

        let T1,T2 be strict TopSpace such that

         A10: the carrier of T1 = X and

         A11: for A be Subset of T1 holds ( Cl A) = ( IFEQ (A, {} ,A,(A \/ ( {x0} /\ X)))) and

         A12: the carrier of T2 = X and

         A13: for A be Subset of T2 holds ( Cl A) = ( IFEQ (A, {} ,A,(A \/ ( {x0} /\ X))));

        now

          let A1 be Subset of T1, A2 be Subset of T2;

          assume A1 = A2;

          

          hence ( Cl A1) = ( IFEQ (A2, {} ,A2,(A2 \/ ( {x0} /\ X)))) by A11

          .= ( Cl A2) by A13;

        end;

        hence thesis by A10, A12, Th8;

      end;

    end

    registration

      let X be non empty set;

      let x0 be set;

      cluster (x0 -PointClTop X) -> non empty;

      coherence by Def7;

    end

    theorem :: TOPGEN_3:37

    

     Th37: for X be non empty set, x0 be Element of X holds for A be non empty Subset of (x0 -PointClTop X) holds ( Cl A) = (A \/ {x0})

    proof

      let X be non empty set;

      let x0 be Element of X;

      let A be non empty Subset of (x0 -PointClTop X);

      

      thus ( Cl A) = ( IFEQ (A, {} ,A,(A \/ ( {x0} /\ X)))) by Def7

      .= (A \/ ( {x0} /\ X)) by FUNCOP_1:def 8

      .= (A \/ {x0}) by XBOOLE_1: 28;

    end;

    theorem :: TOPGEN_3:38

    

     Th38: for X be non empty set, x0 be Element of X holds for A be non empty Subset of (x0 -PointClTop X) holds A is closed iff x0 in A

    proof

      let X be non empty set;

      let x0 be Element of X;

      let A be non empty Subset of (x0 -PointClTop X);

      A is closed iff ( Cl A) = A by PRE_TOPC: 22;

      then A is closed iff A = (A \/ {x0}) by Th37;

      then A is closed iff {x0} c= A by XBOOLE_1: 7, XBOOLE_1: 12;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: TOPGEN_3:39

    

     Th39: for X be non empty set, x0 be Element of X holds for A be proper Subset of (x0 -PointClTop X) holds A is open iff not x0 in A

    proof

      let X be non empty set;

      let x0 be Element of X;

      let A be proper Subset of (x0 -PointClTop X);

      A is open iff (A ` ) is closed by TOPS_1: 4;

      then

       A1: A is open iff x0 in (A ` ) by Th38;

      x0 is Element of (x0 -PointClTop X) by Def7;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: TOPGEN_3:40

    for X,x0,x be set st x0 in X holds {x} is closed Subset of (x0 -PointClTop X) iff x = x0

    proof

      let X,x0,x be set;

      assume

       A1: x0 in X;

      hereby

        assume {x} is closed Subset of (x0 -PointClTop X);

        then x0 in {x} by A1, Th38;

        hence x = x0 by TARSKI:def 1;

      end;

      assume

       A2: x = x0;

      then

       A3: x0 in {x} by ZFMISC_1: 31;

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

      hence thesis by A3, Def7, Th38;

    end;

    theorem :: TOPGEN_3:41

    for X,x0,x be set st {x0} c< X holds {x} is open Subset of (x0 -PointClTop X) iff x in X & x <> x0

    proof

      let X,x0,x be set;

      assume

       A1: {x0} c< X;

      then

      reconsider Y = X as non empty set;

      reconsider A = {x0} as Subset of Y by A1;

      

       A2: x0 in A by TARSKI:def 1;

      reconsider A as proper Subset of Y by A1, SUBSET_1:def 6;

      

       A3: the carrier of (x0 -PointClTop X) = X by Def7;

      hereby

        assume

         A4: {x} is open Subset of (x0 -PointClTop X);

        hence x in X by A3, ZFMISC_1: 31;

        assume x = x0;

        then not x0 in {x0} or A is non proper Subset of (x0 -PointClTop X) by A4, Th39;

        hence contradiction by A3, TARSKI:def 1;

      end;

      assume that

       A5: x in X and

       A6: x <> x0;

      

       A7: not x0 in {x} by A6, TARSKI:def 1;

      x0 in Y by A2;

      then {x} is proper Subset of (x0 -PointClTop Y) by A7, A5, A3, SUBSET_1:def 6, ZFMISC_1: 31;

      hence thesis by A7, A2, Th39;

    end;

    begin

    definition

      let X,X0 be set;

      :: TOPGEN_3:def8

      func X0 -DiscreteTop (X) -> strict TopSpace means

      : Def8: the carrier of it = X & for A be Subset of it holds ( Int A) = ( IFEQ (A,X,A,(A /\ X0)));

      existence

      proof

        deffunc ClOp( set) = ( IFEQ ($1,X,$1,($1 /\ X0)));

        

         A1: for A be Subset of X holds ClOp(A) c= A

        proof

          let A be Subset of X;

          A = X or A <> X;

          then ClOp(A) = A or ClOp(A) = (A /\ X0) by FUNCOP_1:def 8;

          hence thesis by XBOOLE_1: 17;

        end;

        

         A2: for A,B be Subset of X holds ClOp(/\) = ( ClOp(A) /\ ClOp(B))

        proof

          let A,B be Subset of X;

          per cases ;

            suppose

             A3: A = X or B = X;

            

             A4: (B /\ X) = B by XBOOLE_1: 28;

            B = X or B <> X;

            then ClOp(B) = B or ClOp(B) = (B /\ X0) by FUNCOP_1:def 8;

            then

             A5: (X /\ ClOp(B)) = ClOp(B) by XBOOLE_1: 28;

            A = X or A <> X;

            then ClOp(A) = A or ClOp(A) = (A /\ X0) by FUNCOP_1:def 8;

            then

             A6: ( ClOp(A) /\ X) = ClOp(A) by XBOOLE_1: 28;

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

            hence thesis by A4, A6, A5, A3, FUNCOP_1:def 8;

          end;

            suppose

             A7: A <> X & B <> X;

            (A \/ (A /\ B)) = A by XBOOLE_1: 22;

            then (A /\ B) <> X by A7, XBOOLE_1: 12;

            then

             A8: ClOp(/\) = ((A /\ B) /\ X0) by FUNCOP_1:def 8;

            X0 = (X0 /\ X0);

            then ClOp(/\) = (((A /\ B) /\ X0) /\ X0) by A8, XBOOLE_1: 16;

            then

             A9: ClOp(/\) = (((B /\ X0) /\ A) /\ X0) by XBOOLE_1: 16;

            

             A10: ClOp(B) = (B /\ X0) by A7, FUNCOP_1:def 8;

             ClOp(A) = (A /\ X0) by A7, FUNCOP_1:def 8;

            hence thesis by A9, A10, XBOOLE_1: 16;

          end;

        end;

        

         A11: for A be Subset of X holds ClOp(ClOp) = ClOp(A)

        proof

          let A be Subset of X;

          A = X or A <> X;

          then ClOp(A) = X or (A /\ X0) <> X & ClOp(A) = (A /\ X0) by FUNCOP_1:def 8;

          then ClOp(ClOp) = ClOp(A) or ClOp(A) = (A /\ X0) & ClOp(ClOp) = ((A /\ X0) /\ X0) & (X0 /\ X0) = X0 by FUNCOP_1:def 8;

          hence thesis by XBOOLE_1: 16;

        end;

        

         A12: ClOp(X) = X by FUNCOP_1:def 8;

        consider T be strict TopSpace such that

         A13: the carrier of T = X & for A be Subset of T holds ( Int A) = ClOp(A) from TopDefByInteriorOp( A12, A1, A2, A11);

        take T;

        thus the carrier of T = X by A13;

        let F be Subset of T;

        thus thesis by A13;

      end;

      correctness

      proof

        let T1,T2 be strict TopSpace such that

         A14: the carrier of T1 = X and

         A15: for A be Subset of T1 holds ( Int A) = ( IFEQ (A,X,A,(A /\ X0))) and

         A16: the carrier of T2 = X and

         A17: for A be Subset of T2 holds ( Int A) = ( IFEQ (A,X,A,(A /\ X0)));

        now

          let A1 be Subset of T1, A2 be Subset of T2;

          assume A1 = A2;

          

          hence ( Int A1) = ( IFEQ (A2,X,A2,(A2 /\ X0))) by A15

          .= ( Int A2) by A17;

        end;

        hence thesis by A14, A16, Th10;

      end;

    end

    registration

      let X be non empty set;

      let X0 be set;

      cluster (X0 -DiscreteTop X) -> non empty;

      coherence by Def8;

    end

    theorem :: TOPGEN_3:42

    

     Th42: for X be non empty set, X0 be set holds for A be proper Subset of (X0 -DiscreteTop X) holds ( Int A) = (A /\ X0)

    proof

      let X be non empty set, X0 be set;

      let A be proper Subset of (X0 -DiscreteTop X);

      the carrier of (X0 -DiscreteTop X) = X by Def8;

      then

       A1: X <> A by SUBSET_1:def 6;

      

      thus ( Int A) = ( IFEQ (A,X,A,(A /\ X0))) by Def8

      .= (A /\ X0) by A1, FUNCOP_1:def 8;

    end;

    theorem :: TOPGEN_3:43

    

     Th43: for X be non empty set, X0 be set holds for A be proper Subset of (X0 -DiscreteTop X) holds A is open iff A c= X0

    proof

      let X be non empty set, X0 be set;

      let A be proper Subset of (X0 -DiscreteTop X);

      A is open iff ( Int A) = A by TOPS_1: 23;

      then A is open iff A = (A /\ X0) by Th42;

      hence thesis by XBOOLE_1: 17, XBOOLE_1: 28;

    end;

    theorem :: TOPGEN_3:44

    

     Th44: for X be set, X0 be Subset of X holds the topology of (X0 -DiscreteTop X) = ( {X} \/ ( bool X0))

    proof

      let X be set;

      let X0 be Subset of X;

      

       A1: the carrier of (X0 -DiscreteTop X) = X by Def8;

      thus the topology of (X0 -DiscreteTop X) c= ( {X} \/ ( bool X0))

      proof

        let a be object;

        assume

         A2: a in the topology of (X0 -DiscreteTop X);

        then

        reconsider a as Subset of (X0 -DiscreteTop X);

        

         A3: a is proper & X is non empty or not a is proper by A1;

        a is open by A2;

        then a = X or a c= X0 by A3, A1, Th43;

        then a in {X} or a in ( bool X0) by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let a be object;

      reconsider aa = a as set by TARSKI: 1;

      assume a in ( {X} \/ ( bool X0));

      then

       A4: a in {X} or a in ( bool X0) by XBOOLE_0:def 3;

      then a = X or aa c= X0 by TARSKI:def 1;

      then

      reconsider a as Subset of (X0 -DiscreteTop X) by A1, XBOOLE_1: 1;

      assume

       A5: not thesis;

      then

       A6: a <> ( [#] (X0 -DiscreteTop X)) by PRE_TOPC:def 2;

      then

       A7: X is non empty by A1;

      

       A8: a is proper by A6;

      

       A9: not a is open by A5;

      a <> X by A6, Def8;

      hence thesis by A7, A4, A9, A8, Th43, TARSKI:def 1;

    end;

    theorem :: TOPGEN_3:45

    for X be set holds ( ADTS X) = ( {} -DiscreteTop X)

    proof

      let X be set;

      set T = ( {} -DiscreteTop X);

      

       A1: the carrier of T = X by Def8;

      

       A2: ( cobool X) = { {} , X} by TEX_1:def 2;

      

       A3: the topology of T c= ( cobool X)

      proof

        let a be object;

        assume

         A4: a in the topology of T;

        then

        reconsider a as Subset of T;

        a is open by A4;

        then a c= X & X is empty or a is non proper or a c= {} by A1, Th43;

        then a = {} or a = X by A1;

        hence thesis by A2, TARSKI:def 2;

      end;

      ( {} T) = {} ;

      then

       A5: {} in the topology of T by PRE_TOPC:def 2;

      ( [#] T) = X by Def8;

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

      then ( cobool X) c= the topology of T by A5, A2, ZFMISC_1: 32;

      then the topology of T = ( cobool X) by A3;

      hence thesis by A1, TEX_1:def 3;

    end;

    theorem :: TOPGEN_3:46

    for X be set holds ( 1TopSp X) = (X -DiscreteTop X)

    proof

      let X be set;

      set T = (X -DiscreteTop X);

      

       A1: the carrier of T = X by Def8;

      X c= X;

      then the topology of T = ( {X} \/ ( bool X)) by Th44;

      hence thesis by A1, ZFMISC_1: 40;

    end;