:: The Cantor Set
::  by Alexander Yu. Shibakov and Andrzej Trybulec
::
:: Received January 9, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SETFAM_1, SUBSET_1, TARSKI, PRE_TOPC, RCOMP_1, RLVECT_3,
      FINSET_1, XBOOLE_0, FINSUB_1, SETWISEO, ZFMISC_1, STRUCT_0, FUNCT_1,
      RELAT_1, CARD_3, NUMBERS, FUNCOP_1, CARD_1, NAT_1, CANTOR_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, ORDINAL1, NAT_1,
      SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSUB_1, SETWISEO,
      PROB_1, STRUCT_0, PRE_TOPC, TOPS_2, CARD_3, FUNCOP_1;
 constructors SETFAM_1, FUNCOP_1, SETWISEO, CARD_3, TOPS_2, RELSET_1, PROB_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCOP_1, FINSET_1, CARD_3,
      PRE_TOPC, FUNCT_1, TOPS_2;
 requirements BOOLE, SUBSET;
 definitions PRE_TOPC, TARSKI, TOPS_2, XBOOLE_0, STRUCT_0;
 theorems ZFMISC_1, PRE_TOPC, SUBSET_1, SETFAM_1, FINSET_1, FUNCT_2, FUNCT_1,
      TARSKI, FINSUB_1, RELAT_1, XBOOLE_0, XBOOLE_1, TOPS_2, EQREL_1;
 schemes SUBSET_1, FUNCT_2, SETWISEO;

begin

definition
  let X be set;
  let A be Subset-Family of X;
  func UniCl(A) -> Subset-Family of X means
  :Def1:
  for x being Subset of X
  holds x in it iff ex Y being Subset-Family of X st Y c=A & x = union Y;
  existence
  proof
    defpred P[set] means ex Y being Subset-Family of X st Y c= A & $1 = union
    Y;
    ex Z being Subset-Family of X st for x being 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 being Subset of X holds x in F1 iff ex Y being Subset-Family
    of X st Y c=A & x = union Y and
A2: for x being Subset of X holds x in F2 iff ex Y being Subset-Family
    of X st Y c=A & x = union Y;
    now
      let x be Subset of X;
      x in F1 iff ex Y being 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;
  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 set;
    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 Th1:
  for X being set for A being Subset-Family of X holds A c= UniCl A
proof
  let X be set;
  let A be Subset-Family of X;
  let x be set;
  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
  for S being TopStruct holds the topology of S is Basis of S;

theorem
  for S being TopStruct holds the topology of S is open;

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

  func FinMeetCl(A) -> Subset-Family of X means
  :Def3:
  for x being Subset of X holds x in it iff
  ex Y being Subset-Family of X st Y c= A & Y is finite & x = Intersect Y;
  existence
  proof
    defpred P[set] means ex Y being Subset-Family of X st Y c=A & Y is finite
    & $1 = Intersect Y;
    ex Z being Subset-Family of X st for x being 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 being Subset of X holds x in B1 iff ex Y being Subset-Family
    of X st Y c=A & Y is finite & x = Intersect Y and
A2: for x being Subset of X holds x in B2 iff ex Y being 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 being 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 Th4:
  for X being set for A being Subset-Family of X holds A c= FinMeetCl A
proof
  let X be set;
  let A be Subset-Family of X;
  let x be set;
  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 Th5:
  for T being 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 being Element of Fin X, b being 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 being 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 being 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 by SUBSET_1:2;
end;

theorem Th6:
  for T being 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 set;
  assume
A1: a in UniCl the topology of T;
  then reconsider a9 = a as Subset of T;
  ex b being 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 Th7:
  for T being 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 Th8:
  for X being set, A being 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 being Subset-Family of X such that
A1: y = {};
  y c= A & Intersect y = X by A1,SETFAM_1:def 9,XBOOLE_1:2;
  hence thesis by A1,Def3;
end;

theorem Th9:
  for X being set for A, B being 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 set;
  assume
A2: x in UniCl A;
  then reconsider x9 = x as Subset of X;
  consider T being Subset-Family of X such that
A3: T c= A and
A4: x9 = union T by A2,Def1;
  T c=B by A1,A3,XBOOLE_1:1;
  hence thesis by A4,Def1;
end;

theorem Th10:
  for X being set for R being non empty Subset-Family of bool X, F
  being Subset-Family of X st F = { Intersect x where x is Element of R: not
  contradiction} 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 = { Intersect x where x is Element of R: not contradiction};
  hereby
    let c be set;
    assume
A2: c in Intersect F;
    for Y being set st Y in union R holds c in Y
    proof
      let Y be set;
      assume Y in union R;
      then consider d being 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 set;
  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 being 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 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[set,set] means ex A being Subset-Family of X st $1 = Intersect A &
  A = $2 & $2 is finite;
  thus FinMeetCl A c= FinMeetCl FinMeetCl A by Th4;
  let x be set;
  assume
A1: x in FinMeetCl FinMeetCl A;
  then reconsider x9 = x as Subset of X;
  consider Y being 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 being set st e in Y ex u being set st u in bool A & P[e,u]
  proof
    let e be set;
    assume
A6: e in Y;
    then reconsider e9 = e as Subset of X;
    consider Y being 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 being Function of Y, bool A such that
A8: for e being set st e in Y holds P[e,f.e] from FUNCT_2:sch 1(A5);
  set fz = { Intersect s where s is Subset-Family of X: s in rng f};
A9: fz c= Y
  proof
    let l be set;
    assume l in fz;
    then consider s being Subset-Family of X such that
A10: l = Intersect s and
A11: s in rng f;
    consider v being set 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 set;
    assume
A15: l in Y;
    then consider C being Subset-Family of X such that
A16: l = Intersect C and
A17: C = f.l and
    f.l 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,XBOOLE_0:def 10;
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 = { Intersect b where b is Element of GGG: not contradiction}
      proof
        hereby
          let x be set;
          assume x in fz;
          then ex s being Subset-Family of X st x = Intersect s & s in rng f;
          hence
          x in { Intersect b where b is Element of GGG: not contradiction };
        end;
        let x be set;
        assume
        x in { Intersect b where b is Element of GGG: not contradiction};
        then ex s being 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,41,ZFMISC_1:2;
    end;
  end;
  for V being set st V in rng f holds V is finite
  proof
    let V be set;
    assume V in rng f;
    then consider x being set 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
  for X being set, A being Subset-Family of X, a, b being 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 Th13:
  for X being set, A being Subset-Family of X, a, b being 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 set;
  assume Z in INTERSECTION(a,b);
  then consider V, B being 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 Th14:
  for X being set, A,B being 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 set;
  assume
A2: x in FinMeetCl A;
  then reconsider x as Subset of X;
  consider y being 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,XBOOLE_1:1;
  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 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 being 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 being Subset of T st c in a & c = union $1;
    consider b being Subset-Family of FinMeetCl A such that
A3: for B being Subset of FinMeetCl A holds B in b iff P[B] from
    SUBSET_1:sch 3;
A4: a = { union B where B is Subset of FinMeetCl A: B in b }
    proof
      set gh = { union B where B is Subset of FinMeetCl A: B in b };
      hereby
        let x be set;
        assume
A5:     x in a;
        then reconsider x9 = x as Subset of X;
        consider V being 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 set;
      assume x in gh;
      then consider B being Subset of FinMeetCl A such that
A8:   x = union B and
A9:   B in b;
      ex c being 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 is 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 being 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 being 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;
  attr F is quasi_prebasis means
:Def4:
  ex G being Basis of X st G c= FinMeetCl F;
end;

registration
  let X be TopStruct;
  cluster the topology of X -> quasi_prebasis;
  coherence
  proof
    take the topology of X;
    thus thesis by Th4;
  end;
  cluster -> quasi_prebasis for Basis of X;
  coherence
  proof
    let F be Basis of X;
    take F;
    thus thesis by Th4;
  end;
  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 Th16:
  for X being non empty set, Y being Subset-Family of X holds
  Y is Basis of TopStruct (#X, UniCl Y#)
proof
  let X be non empty set, Y be Subset-Family of X;
  Y c= UniCl Y by Th1;
  hence thesis by Def2,TOPS_2:64;
end;

theorem Th17:
  for T1, T2 being strict non empty TopSpace, P being 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 being 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,XBOOLE_1:1;
  consider B2 being 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,XBOOLE_1:1;
  the topology of T2 = UniCl FinMeetCl the topology of T2 by Th7;
  then
A11: UniCl FinMeetCl P9 = the topology of T2 by A10,A5,XBOOLE_0:def 10;
  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 Th18:
  for X being non empty set, Y being 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 by XBOOLE_1:1;
    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
  func the_Cantor_set -> strict non empty TopSpace means
  the carrier of it = product (NAT-->{0,1}) &
  ex P being prebasis of it st for X being Subset of product (NAT-->{0,1})
  holds X in P iff ex N,n being Nat st
  for F being Element of product (NAT-->{0,1}) holds F in X iff F.N=n;
  existence
  proof
    defpred P[set] means ex N,n being Nat st for F being Element of product (
    NAT-->{0,1}) holds F in $1 iff F.N=n;
    consider Y being Subset-Family of product(NAT-->{0,1}) such that
A1: for y being 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 being prebasis of T1 st for X being Subset of product (NAT-->
{0 ,1}) holds X in P iff ex N,n being Nat st for F being 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 being prebasis of T2 st for X being Subset of product (NAT-->
{0 ,1}) holds X in P iff ex N,n being Nat st for F being Element of product (
    NAT -->{0,1}) holds F in X iff F.N=n;
    consider P1 being prebasis of T1 such that
A6: for X being Subset of product (NAT-->{0,1}) holds X in P1 iff ex N
,n being Nat st for F being Element of product (NAT-->{0,1}) holds F in X iff F
    .N=n by A3;
    consider P2 being prebasis of T2 such that
A7: for X being Subset of product (NAT-->{0,1}) holds X in P2 iff ex N
,n being Nat st for F being 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 being Nat st for F being 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;
 
:: the aim is to prove: theorem the_Cantor_set is compact