cantor_1.miz

    begin

    definition

      let X be set;

      let A be Subset-Family of X;

      :: CANTOR_1:def1

      func UniCl (A) -> Subset-Family of X means

      : Def1: for x be Subset of X holds x in it iff ex Y be Subset-Family of X st Y c= A & x = ( union Y);

      existence

      proof

        defpred P[ set] means ex Y be Subset-Family of X st Y c= A & $1 = ( union Y);

        ex Z be Subset-Family of X st for x be Subset of X holds x in Z iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Subset-Family of X such that

         A1: for x be Subset of X holds x in F1 iff ex Y be Subset-Family of X st Y c= A & x = ( union Y) and

         A2: for x be Subset of X holds x in F2 iff ex Y be Subset-Family of X st Y c= A & x = ( union Y);

        now

          let x be Subset of X;

          x in F1 iff ex Y be Subset-Family of X st Y c= A & x = ( union Y) by A1;

          hence x in F1 iff x in F2 by A2;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    definition

      let X be TopStruct, F be Subset-Family of X;

      :: CANTOR_1:def2

      attr F is quasi_basis means

      : Def2: the topology of X c= ( UniCl F);

    end

    registration

      let X be TopStruct;

      cluster the topology of X -> quasi_basis;

      coherence

      proof

        set F = the topology of X;

        let A be object;

        assume

         A1: A in F;

        then

        reconsider B = {A} as Subset-Family of X by SUBSET_1: 41;



         A2: B c= F by A1, ZFMISC_1: 31;

        A = ( union B) by ZFMISC_1: 25;

        hence A in ( UniCl F) by A2, Def1;

      end;

    end

    registration

      let X be TopStruct;

      cluster open quasi_basis for Subset-Family of X;

      existence

      proof

        take the topology of X;

        thus thesis;

      end;

    end

    definition

      let X be TopStruct;

      mode Basis of X is open quasi_basis Subset-Family of X;

    end

    theorem :: CANTOR_1:1



     Th1: for X be set holds for A be Subset-Family of X holds A c= ( UniCl A)

    proof

      let X be set;

      let A be Subset-Family of X;

      let x be object;

      assume

       A1: x in A;

      then

      reconsider x9 = x as Subset of X;

      reconsider s = {x9} as Subset-Family of X by SUBSET_1: 41;



       A2: x = ( union s) by ZFMISC_1: 25;

      s c= A by A1, ZFMISC_1: 31;

      hence thesis by A2, Def1;

    end;

    theorem :: CANTOR_1:2

    for S be TopStruct holds the topology of S is Basis of S;

    theorem :: CANTOR_1:3

    for S be TopStruct holds the topology of S is open;

    definition

      let X be set;

      let A be Subset-Family of X;

      :: CANTOR_1:def3

      func FinMeetCl (A) -> Subset-Family of X means

      : Def3: for x be Subset of X holds x in it iff ex Y be Subset-Family of X st Y c= A & Y is finite & x = ( Intersect Y);

      existence

      proof

        defpred P[ set] means ex Y be Subset-Family of X st Y c= A & Y is finite & $1 = ( Intersect Y);

        ex Z be Subset-Family of X st for x be Subset of X holds x in Z iff P[x] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let B1,B2 be Subset-Family of X such that

         A1: for x be Subset of X holds x in B1 iff ex Y be Subset-Family of X st Y c= A & Y is finite & x = ( Intersect Y) and

         A2: for x be Subset of X holds x in B2 iff ex Y be Subset-Family of X st Y c= A & Y is finite & x = ( Intersect Y);

        now

          let x be Subset of X;

          x in B2 iff ex Y be Subset-Family of X st Y c= A & Y is finite & x = ( Intersect Y) by A2;

          hence x in B2 iff x in B1 by A1;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    theorem :: CANTOR_1:4



     Th4: for X be set holds for A be Subset-Family of X holds A c= ( FinMeetCl A)

    proof

      let X be set;

      let A be Subset-Family of X;

      let x be object;

      assume

       A1: x in A;

      then

      reconsider x9 = x as Subset of X;

      reconsider s = {x9} as Subset-Family of X by SUBSET_1: 41;

      x = ( meet s) by SETFAM_1: 10;

      then

       A2: x = ( Intersect s) by SETFAM_1:def 9;

      s c= A by A1, ZFMISC_1: 31;

      hence thesis by A2, Def3;

    end;

    theorem :: CANTOR_1:5



     Th5: for T be non empty TopSpace holds the topology of T = ( FinMeetCl the topology of T)

    proof

      let T be non empty TopSpace;

      set X = the topology of T;

      defpred P[ set] means ( meet $1) in the topology of T;



       A1: for B9 be Element of ( Fin X), b be Element of X holds P[B9] implies P[(B9 \/ {b})]

      proof

        let B9 be Element of ( Fin X), b be Element of X;



         A2: ( meet {b}) = b by SETFAM_1: 10;

        assume

         A3: ( meet B9) in X;

        per cases ;

          suppose B9 <> {} ;

          then ( meet (B9 \/ {b})) = (( meet B9) /\ ( meet {b})) by SETFAM_1: 9;

          hence thesis by A2, A3, PRE_TOPC:def 1;

        end;

          suppose B9 = {} ;

          hence thesis by A2;

        end;

      end;

      thus the topology of T c= ( FinMeetCl the topology of T) by Th4;



       A4: P[( {}. X)] by PRE_TOPC: 1, SETFAM_1: 1;



       A5: for B be Element of ( Fin X) holds P[B] from SETWISEO:sch 4( A4, A1);

      now

        let x be Subset of T;

        assume x in ( FinMeetCl X);

        then

        consider y be Subset-Family of T such that

         A6: y c= X & y is finite and

         A7: x = ( Intersect y) by Def3;

        reconsider y as Subset-Family of T;

        per cases ;

          suppose

           A8: y <> {} ;



           A9: y in ( Fin X) by A6, FINSUB_1:def 5;

          x = ( meet y) by A7, A8, SETFAM_1:def 9;

          hence x in X by A5, A9;

        end;

          suppose

           A10: y = {} ;

          reconsider aa = ( {} ( bool the carrier of T)) as Subset-Family of the carrier of T;

          ( Intersect aa) = the carrier of T by SETFAM_1:def 9;

          hence x in X by A7, A10, PRE_TOPC:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: CANTOR_1:6



     Th6: for T be TopSpace holds the topology of T = ( UniCl the topology of T)

    proof

      let T be TopSpace;

      thus the topology of T c= ( UniCl the topology of T) by Th1;

      let a be object;

      assume

       A1: a in ( UniCl the topology of T);

      then

      reconsider a9 = a as Subset of T;

      ex b be Subset-Family of T st b c= the topology of T & a9 = ( union b) by A1, Def1;

      hence thesis by PRE_TOPC:def 1;

    end;

    theorem :: CANTOR_1:7



     Th7: for T be non empty TopSpace holds the topology of T = ( UniCl ( FinMeetCl the topology of T))

    proof

      let T be non empty TopSpace;

      the topology of T = ( FinMeetCl the topology of T) by Th5;

      hence thesis by Th6;

    end;

    theorem :: CANTOR_1:8



     Th8: for X be set, A be Subset-Family of X holds X in ( FinMeetCl A)

    proof

      let X be set, A be Subset-Family of X;

       {} is Subset-Family of X by XBOOLE_1: 2;

      then

      consider y be Subset-Family of X such that

       A1: y = {} ;

      y c= A & ( Intersect y) = X by A1, SETFAM_1:def 9;

      hence thesis by A1, Def3;

    end;

    theorem :: CANTOR_1:9



     Th9: for X be set holds for A,B be Subset-Family of X holds A c= B implies ( UniCl A) c= ( UniCl B)

    proof

      let X be set;

      let A,B be Subset-Family of X such that

       A1: A c= B;

      let x be object;

      assume

       A2: x in ( UniCl A);

      then

      reconsider x9 = x as Subset of X;

      consider T be Subset-Family of X such that

       A3: T c= A and

       A4: x9 = ( union T) by A2, Def1;

      T c= B by A1, A3;

      hence thesis by A4, Def1;

    end;

    theorem :: CANTOR_1:10



     Th10: for X be set holds for R be non empty Subset-Family of ( bool X), F be Subset-Family of X st F = the set of all ( Intersect x) where x be Element of R holds ( Intersect F) = ( Intersect ( union R))

    proof

      let X be set;

      let R be non empty Subset-Family of ( bool X), F be Subset-Family of X such that

       A1: F = the set of all ( Intersect x) where x be Element of R;

      hereby

        let c be object;

        assume

         A2: c in ( Intersect F);

        for Y be set st Y in ( union R) holds c in Y

        proof

          let Y be set;

          assume Y in ( union R);

          then

          consider d be set such that

           A3: Y in d and

           A4: d in R by TARSKI:def 4;

          reconsider d as Subset-Family of X by A4;

          reconsider d as Subset-Family of X;

          ( Intersect d) in F by A1, A4;

          then c in ( Intersect d) by A2, SETFAM_1: 43;

          hence thesis by A3, SETFAM_1: 43;

        end;

        hence c in ( Intersect ( union R)) by A2, SETFAM_1: 43;

      end;

      let c be object;

      assume

       A5: c in ( Intersect ( union R));

      for Y be set st Y in F holds c in Y

      proof

        let Y be set;

        assume Y in F;

        then

        consider x be Element of R such that

         A6: Y = ( Intersect x) by A1;

        ( Intersect ( union R)) c= ( Intersect x) by SETFAM_1: 44, ZFMISC_1: 74;

        hence thesis by A5, A6;

      end;

      hence thesis by A5, SETFAM_1: 43;

    end;

    theorem :: CANTOR_1:11



     Th11: for X be set, A be Subset-Family of X holds ( FinMeetCl A) = ( FinMeetCl ( FinMeetCl A))

    proof

      let X be set, A be Subset-Family of X;

      defpred P[ object, object] means ex A be Subset-Family of X st $1 = ( Intersect A) & A = $2 & A is finite;

      thus ( FinMeetCl A) c= ( FinMeetCl ( FinMeetCl A)) by Th4;

      let x be object;

      assume

       A1: x in ( FinMeetCl ( FinMeetCl A));

      then

      reconsider x9 = x as Subset of X;

      consider Y be Subset-Family of X such that

       A2: Y c= ( FinMeetCl A) and

       A3: Y is finite and

       A4: x9 = ( Intersect Y) by A1, Def3;



       A5: for e be object st e in Y holds ex u be object st u in ( bool A) & P[e, u]

      proof

        let e be object;

        assume

         A6: e in Y;

        then

        reconsider e9 = e as Subset of X;

        consider Y be Subset-Family of X such that

         A7: Y c= A & Y is finite & e9 = ( Intersect Y) by A2, A6, Def3;

        take Y;

        thus thesis by A7;

      end;

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

       A8: for e be object st e in Y holds P[e, (f . e)] from FUNCT_2:sch 1( A5);

      set fz = { ( Intersect s) where s be Subset-Family of X : s in ( rng f) };



       A9: fz c= Y

      proof

        let l be object;

        assume l in fz;

        then

        consider s be Subset-Family of X such that

         A10: l = ( Intersect s) and

         A11: s in ( rng f);

        consider v be object such that

         A12: v in ( dom f) and

         A13: s = (f . v) by A11, FUNCT_1:def 3;

        v in Y by A12, FUNCT_2:def 1;

        then P[v, (f . v)] by A8;

        hence thesis by A10, A12, A13, FUNCT_2:def 1;

      end;

      ( rng f) c= ( bool A) by RELAT_1:def 19;

      then ( union ( rng f)) c= ( union ( bool A)) by ZFMISC_1: 77;

      then

       A14: ( union ( rng f)) c= A by ZFMISC_1: 81;

      then

      reconsider y = ( union ( rng f)) as Subset-Family of X by XBOOLE_1: 1;

      reconsider y as Subset-Family of X;

      Y c= fz

      proof

        let l be object;

        assume

         A15: l in Y;

        then

        consider C be Subset-Family of X such that

         A16: l = ( Intersect C) and

         A17: C = (f . l) and C is finite by A8;

        l in ( dom f) by A15, FUNCT_2:def 1;

        then C in ( rng f) by A17, FUNCT_1:def 3;

        hence thesis by A16;

      end;

      then

       A18: Y = fz by A9;



       A19: x = ( Intersect y)

      proof

        per cases ;

          suppose

           A20: ( rng f) <> {} ;

          ( rng f) c= ( bool A) & ( bool A) c= ( bool ( bool X)) by RELAT_1:def 19, ZFMISC_1: 67;

          then

          reconsider GGG = ( rng f) as non empty Subset-Family of ( bool X) by A20, XBOOLE_1: 1;

          reconsider GGG as non empty Subset-Family of ( bool X);

          fz = the set of all ( Intersect b) where b be Element of GGG

          proof

            hereby

              let x be object;

              assume x in fz;

              then ex s be Subset-Family of X st x = ( Intersect s) & s in ( rng f);

              hence x in the set of all ( Intersect b) where b be Element of GGG;

            end;

            let x be object;

            assume x in the set of all ( Intersect b) where b be Element of GGG;

            then ex s be Element of GGG st x = ( Intersect s);

            hence thesis;

          end;

          hence thesis by A4, A18, Th10;

        end;

          suppose

           A21: ( rng f) = {} ;

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

          hence thesis by A4, A21, RELAT_1: 38, RELAT_1: 41, ZFMISC_1: 2;

        end;

      end;

      for V be set st V in ( rng f) holds V is finite

      proof

        let V be set;

        assume V in ( rng f);

        then

        consider x be object such that

         A22: x in ( dom f) and

         A23: V = (f . x) by FUNCT_1:def 3;

        x in Y by A22, FUNCT_2:def 1;

        then

        reconsider x as Subset of X;

        reconsider G = (f . x) as Subset-Family of X;

        x in Y by A22, FUNCT_2:def 1;

        then P[x, G] by A8;

        hence thesis by A23;

      end;

      then ( union ( rng f)) is finite by A3, FINSET_1: 7;

      hence thesis by A14, A19, Def3;

    end;

    theorem :: CANTOR_1:12

    for X be set, A be Subset-Family of X, a,b be set st a in ( FinMeetCl A) & b in ( FinMeetCl A) holds (a /\ b) in ( FinMeetCl A)

    proof

      let X be set, A be Subset-Family of X, a,b be set;

      assume

       A1: a in ( FinMeetCl A) & b in ( FinMeetCl A);

      then

      reconsider M = {a, b} as Subset-Family of X by ZFMISC_1: 32;

      reconsider M as Subset-Family of X;

      (a /\ b) = ( meet M) by SETFAM_1: 11;

      then

       A2: (a /\ b) = ( Intersect M) by SETFAM_1:def 9;

      M c= ( FinMeetCl A) by A1, ZFMISC_1: 32;

      then ( Intersect M) in ( FinMeetCl ( FinMeetCl A)) by Def3;

      hence thesis by A2, Th11;

    end;

    theorem :: CANTOR_1:13



     Th13: for X be set, A be Subset-Family of X, a,b be set st a c= ( FinMeetCl A) & b c= ( FinMeetCl A) holds ( INTERSECTION (a,b)) c= ( FinMeetCl A)

    proof

      let X be set;

      let A be Subset-Family of X;

      let a,b be set such that

       A1: a c= ( FinMeetCl A) & b c= ( FinMeetCl A);

      let Z be object;

      assume Z in ( INTERSECTION (a,b));

      then

      consider V,B be set such that

       A2: V in a & B in b and

       A3: Z = (V /\ B) by SETFAM_1:def 5;

      V in ( FinMeetCl A) & B in ( FinMeetCl A) by A1, A2;

      then

      reconsider M = {V, B} as Subset-Family of X by ZFMISC_1: 32;

      reconsider M as Subset-Family of X;

      (V /\ B) = ( meet M) by SETFAM_1: 11;

      then

       A4: (V /\ B) = ( Intersect M) by SETFAM_1:def 9;

      M c= ( FinMeetCl A) by A1, A2, ZFMISC_1: 32;

      then ( Intersect M) in ( FinMeetCl ( FinMeetCl A)) by Def3;

      hence thesis by A3, A4, Th11;

    end;

    theorem :: CANTOR_1:14



     Th14: for X be set, A,B be Subset-Family of X holds A c= B implies ( FinMeetCl A) c= ( FinMeetCl B)

    proof

      let X be set, A,B be Subset-Family of X such that

       A1: A c= B;

      let x be object;

      assume

       A2: x in ( FinMeetCl A);

      then

      reconsider x as Subset of X;

      consider y be Subset-Family of X such that

       A3: y c= A and

       A4: y is finite & x = ( Intersect y) by A2, Def3;

      y c= B by A1, A3;

      hence thesis by A4, Def3;

    end;

    registration

      let X be set;

      let A be Subset-Family of X;

      cluster ( FinMeetCl A) -> non empty;

      coherence by Th8;

    end

    theorem :: CANTOR_1:15



     Th15: for X be non empty set, A be Subset-Family of X holds TopStruct (# X, ( UniCl ( FinMeetCl A)) #) is TopSpace-like

    proof

      let X be non empty set, A be Subset-Family of X;

      set T = TopStruct (# X, ( UniCl ( FinMeetCl A)) #);



       A1: ( [#] T) in ( FinMeetCl A) by Th8;

      now

        reconsider Y = {( [#] T)} as Subset-Family of X by ZFMISC_1: 68;

        reconsider Y as Subset-Family of X;

        take Y;

        thus Y c= ( FinMeetCl A) by A1, ZFMISC_1: 31;

        thus ( [#] T) = ( union Y) by ZFMISC_1: 25;

      end;

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

      thus for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T

      proof

        let a be Subset-Family of T such that

         A2: a c= the topology of T;

        defpred P[ set] means ex c be Subset of T st c in a & c = ( union $1);

        consider b be Subset-Family of ( FinMeetCl A) such that

         A3: for B be Subset of ( FinMeetCl A) holds B in b iff P[B] from SUBSET_1:sch 3;



         A4: a = { ( union B) where B be Subset of ( FinMeetCl A) : B in b }

        proof

          set gh = { ( union B) where B be Subset of ( FinMeetCl A) : B in b };

          hereby

            let x be object;

            assume

             A5: x in a;

            then

            reconsider x9 = x as Subset of X;

            consider V be Subset-Family of X such that

             A6: V c= ( FinMeetCl A) and

             A7: x9 = ( union V) by A2, A5, Def1;

            V in b by A3, A5, A6, A7;

            hence x in gh by A7;

          end;

          let x be object;

          assume x in gh;

          then

          consider B be Subset of ( FinMeetCl A) such that

           A8: x = ( union B) and

           A9: B in b;

          ex c be Subset of T st c in a & c = ( union B) by A3, A9;

          hence thesis by A8;

        end;

        ( union ( union b)) = ( union { ( union B) where B be Subset of ( FinMeetCl A) : B in b }) & ( union b) c= ( bool X) by EQREL_1: 54, XBOOLE_1: 1;

        hence thesis by A4, Def1;

      end;

      let a,b be Subset of T;

      assume a in the topology of T;

      then

      consider F be Subset-Family of X such that

       A10: F c= ( FinMeetCl A) and

       A11: a = ( union F) by Def1;

      assume b in the topology of T;

      then

      consider G be Subset-Family of X such that

       A12: G c= ( FinMeetCl A) and

       A13: b = ( union G) by Def1;



       A14: ( union ( INTERSECTION (F,G))) = (a /\ b) by A11, A13, SETFAM_1: 28;



       A15: ( INTERSECTION (F,G)) c= ( FinMeetCl A) by A10, A12, Th13;

      then ( INTERSECTION (F,G)) is Subset-Family of X by XBOOLE_1: 1;

      hence thesis by A15, A14, Def1;

    end;

    definition

      let X be TopStruct, F be Subset-Family of X;

      :: CANTOR_1:def4

      attr F is quasi_prebasis means

      : Def4: ex G be Basis of X st G c= ( FinMeetCl F);

    end

    registration

      let X be TopStruct;

      cluster the topology of X -> quasi_prebasis;

      coherence by Th4;

      cluster -> quasi_prebasis for Basis of X;

      coherence by Th4;

      cluster open quasi_prebasis for Subset-Family of X;

      existence

      proof

        take the topology of X;

        thus thesis;

      end;

    end

    definition

      let X be TopStruct;

      mode prebasis of X is open quasi_prebasis Subset-Family of X;

    end

    theorem :: CANTOR_1:16



     Th16: for X be non empty set, Y be Subset-Family of X holds Y is Basis of TopStruct (# X, ( UniCl Y) #) by Def2, Th1, TOPS_2: 64;

    theorem :: CANTOR_1:17



     Th17: for T1,T2 be strict non empty TopSpace, P be prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds T1 = T2

    proof

      let T1,T2 be strict non empty TopSpace, P be prebasis of T1 such that

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

       A2: P is prebasis of T2;

      reconsider P9 = P as prebasis of T2 by A2;

      consider B1 be Basis of T1 such that

       A3: B1 c= ( FinMeetCl P) by Def4;

      P c= the topology of T1 by TOPS_2: 64;

      then ( FinMeetCl P) c= ( FinMeetCl the topology of T1) by Th14;

      then

       A4: ( UniCl ( FinMeetCl P)) c= ( UniCl ( FinMeetCl the topology of T1)) by Th9;

      P9 c= the topology of T2 by TOPS_2: 64;

      then ( FinMeetCl P9) c= ( FinMeetCl the topology of T2) by Th14;

      then

       A5: ( UniCl ( FinMeetCl P9)) c= ( UniCl ( FinMeetCl the topology of T2)) by Th9;



       A6: the topology of T1 c= ( UniCl B1) by Def2;

      ( UniCl B1) c= ( UniCl ( FinMeetCl P)) by A3, Th9;

      then

       A7: the topology of T1 c= ( UniCl ( FinMeetCl P)) by A6;

      consider B2 be Basis of T2 such that

       A8: B2 c= ( FinMeetCl P9) by Def4;



       A9: the topology of T2 c= ( UniCl B2) by Def2;

      ( UniCl B2) c= ( UniCl ( FinMeetCl P9)) by A8, Th9;

      then

       A10: the topology of T2 c= ( UniCl ( FinMeetCl P9)) by A9;

      the topology of T2 = ( UniCl ( FinMeetCl the topology of T2)) by Th7;

      then

       A11: ( UniCl ( FinMeetCl P9)) = the topology of T2 by A10, A5;

      the topology of T1 = ( UniCl ( FinMeetCl the topology of T1)) by Th7;

      hence thesis by A1, A7, A11, A4, XBOOLE_0:def 10;

    end;

    theorem :: CANTOR_1:18



     Th18: for X be non empty set, Y be Subset-Family of X holds Y is prebasis of TopStruct (# X, ( UniCl ( FinMeetCl Y)) #)

    proof

      let X be non empty set, A be Subset-Family of X;

      set T = TopStruct (# X, ( UniCl ( FinMeetCl A)) #);

      reconsider A9 = A as Subset-Family of T;

      now

        A9 c= ( FinMeetCl A) & ( FinMeetCl A) c= the topology of T by Th1, Th4;

        then A9 c= the topology of T;

        hence A9 is open by TOPS_2: 64;

        thus A9 is quasi_prebasis

        proof

          reconsider B = ( FinMeetCl A9) as Basis of T by Th16;

          take B;

          thus thesis;

        end;

      end;

      hence thesis;

    end;

    definition

      :: CANTOR_1:def5

      func the_Cantor_set -> strict non empty TopSpace means the carrier of it = ( product ( NAT --> { 0 , 1})) & ex P be prebasis of it st for X be Subset of ( product ( NAT --> { 0 , 1})) holds X in P iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in X iff (F . N) = n;

      existence

      proof

        defpred P[ set] means ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in $1 iff (F . N) = n;

        consider Y be Subset-Family of ( product ( NAT --> { 0 , 1})) such that

         A1: for y be Subset of ( product ( NAT --> { 0 , 1})) holds y in Y iff P[y] from SUBSET_1:sch 3;

        reconsider T = TopStruct (# ( product ( NAT --> { 0 , 1})), ( UniCl ( FinMeetCl Y)) #) as strict non empty TopSpace by Th15;

        take T;

        thus the carrier of T = ( product ( NAT --> { 0 , 1}));

        reconsider Y as prebasis of T by Th18;

        take Y;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let T1,T2 be strict non empty TopSpace such that

         A2: the carrier of T1 = ( product ( NAT --> { 0 , 1})) and

         A3: ex P be prebasis of T1 st for X be Subset of ( product ( NAT --> { 0 , 1})) holds X in P iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in X iff (F . N) = n and

         A4: the carrier of T2 = ( product ( NAT --> { 0 , 1})) and

         A5: ex P be prebasis of T2 st for X be Subset of ( product ( NAT --> { 0 , 1})) holds X in P iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in X iff (F . N) = n;

        consider P1 be prebasis of T1 such that

         A6: for X be Subset of ( product ( NAT --> { 0 , 1})) holds X in P1 iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in X iff (F . N) = n by A3;

        consider P2 be prebasis of T2 such that

         A7: for X be Subset of ( product ( NAT --> { 0 , 1})) holds X in P2 iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in X iff (F . N) = n by A5;

        now

          let x be Subset of ( product ( NAT --> { 0 , 1}));

          x in P1 iff ex N,n be Nat st for F be Element of ( product ( NAT --> { 0 , 1})) holds F in x iff (F . N) = n by A6;

          hence x in P1 iff x in P2 by A7;

        end;

        then P1 = P2 by A2, A4, SUBSET_1: 3;

        hence thesis by A2, A4, Th17;

      end;

    end