:: CANTOR_1 semantic presentation

begin

definition
let X be set ;
let A be Subset-Family of X;
func UniCl A ->  Subset-Family of X means :Def1: :: CANTOR_1:def 1
 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
 ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of X st ( for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds
( x in b2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of X; ::_thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies F1 = F2 )
assume 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 ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Subset_of_X_holds_
(_x_in_F1_iff_x_in_F2_)
let x be Subset of X; ::_thesis: ( x in F1 iff x in F2 )
 ( 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; ::_thesis: verum
end;
hence  F1 = F2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines UniCl CANTOR_1:def_1_:_
 for X being set
for A, b3 being Subset-Family of X holds
( b3 = UniCl A iff for x being Subset of X holds
( x in b3 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) );

definition
let X be TopStruct ;
let F be Subset-Family of X;
attrF is quasi_basis  means :Def2: :: CANTOR_1:def 2
 the topology of X c= UniCl F;
end;

:: deftheorem Def2 defines quasi_basis CANTOR_1:def_2_:_
 for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_basis iff the topology of X c= UniCl F );

registration
let X be TopStruct ;
cluster the topology of X ->  quasi_basis ;
coherence
 the topology of X is quasi_basis
proof
set F = the topology of X;
let A be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not A in the topology of X or A in UniCl the topology of X )
assume A1: A in the topology of X ; ::_thesis: A in UniCl the topology of X
then reconsider B = {A} as Subset-Family of X by SUBSET_1:41;
A2: B c= the topology of X by A1, ZFMISC_1:31;
 A = union B by ZFMISC_1:25;
hence  A in UniCl the topology of X by A2, Def1; ::_thesis: verum
end;
end;

registration
let X be TopStruct ;
cluster open quasi_basis for Element of bool (bool the carrier of X);
existence
 ex b1 being Subset-Family of X st
( b1 is open & b1 is quasi_basis )
proof
take  the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_basis )
thus  ( the topology of X is open & the topology of X is quasi_basis ) ; ::_thesis: verum
end;
end;

definition
let X be TopStruct ;
mode Basis of X is open quasi_basis Subset-Family of X;
end;

theorem Th1: :: CANTOR_1:1
for X being set
for A being Subset-Family of X holds A c= UniCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds A c= UniCl A
let A be Subset-Family of X; ::_thesis: A c= UniCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in UniCl A )
assume A1: x in A ; ::_thesis: x in UniCl 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  x in UniCl A by A2, Def1; ::_thesis: verum
end;

theorem :: CANTOR_1:2
for S being TopStruct holds the topology of S is Basis of S ;

theorem :: CANTOR_1:3
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: :: CANTOR_1:def 3
 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
 ex b1 being Subset-Family of X st
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 ) )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of X st
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 ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of X st ( 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 ) ) ) & ( 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 ) ) ) holds
b1 = b2
proof
let B1, B2 be Subset-Family of X; ::_thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies B1 = B2 )
assume 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 ) ) ; ::_thesis: B1 = B2
now__::_thesis:_for_x_being_Subset_of_X_holds_
(_x_in_B2_iff_x_in_B1_)
let x be Subset of X; ::_thesis: ( x in B2 iff x in B1 )
 ( 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; ::_thesis: verum
end;
hence  B1 = B2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines FinMeetCl CANTOR_1:def_3_:_
 for X being set
for A, b3 being Subset-Family of X holds
( b3 = FinMeetCl A iff for x being Subset of X holds
( x in b3 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) );

theorem Th4: :: CANTOR_1:4
for X being set
for A being Subset-Family of X holds A c= FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds A c= FinMeetCl A
let A be Subset-Family of X; ::_thesis: A c= FinMeetCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in FinMeetCl A )
assume A1: x in A ; ::_thesis: x in FinMeetCl 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  x in FinMeetCl A by A2, Def3; ::_thesis: verum
end;

theorem Th5: :: CANTOR_1:5
for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T
proof
let T be non empty TopSpace; ::_thesis: the topology of T = FinMeetCl the topology of T
set X = the topology of T;
defpred S1[ set ] means  meet $1 in the topology of T;
A1: for B9 being Element of Fin the topology of T
for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin the topology of T; ::_thesis: for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
let b be Element of the topology of T; ::_thesis: ( S1[B9] implies S1[B9 \/ {b}] )
A2: meet {b} = b by SETFAM_1:10;
assume A3: meet B9 in the topology of T ; ::_thesis: S1[B9 \/ {b}]
percases ( B9 <> {} or B9 = {} ) ;
suppose B9 <> {} ; ::_thesis: S1[B9 \/ {b}]
then  meet (B9 \/ {b}) = (meet B9) /\ (meet {b}) by SETFAM_1:9;
hence  S1[B9 \/ {b}] by A2, A3, PRE_TOPC:def_1; ::_thesis: verum
end;
suppose B9 = {} ; ::_thesis: S1[B9 \/ {b}]
hence  S1[B9 \/ {b}] by A2; ::_thesis: verum
end;
end;
end;
thus  the topology of T c= FinMeetCl the topology of T by Th4; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl the topology of T c= the topology of T
A4: S1[ {}. the topology of T] by PRE_TOPC:1, SETFAM_1:1;
A5: for B being Element of Fin the topology of T holds S1[B] from SETWISEO:sch_4(A4, A1);
now__::_thesis:_for_x_being_Subset_of_T_st_x_in_FinMeetCl_the_topology_of_T_holds_
x_in_the_topology_of_T
let x be Subset of T; ::_thesis: ( x in FinMeetCl the topology of T implies b1 in the topology of T )
assume  x in FinMeetCl the topology of T ; ::_thesis: b1 in the topology of T
then consider y being Subset-Family of T such that
A6: ( y c= the topology of T & y is finite ) and
A7: x = Intersect y by Def3;
reconsider y = y as Subset-Family of T ;
percases ( y <> {} or y = {} ) ;
supposeA8: y <> {} ; ::_thesis: b1 in the topology of T
A9: y in Fin the topology of T by A6, FINSUB_1:def_5;
 x = meet y by A7, A8, SETFAM_1:def_9;
hence  x in the topology of T by A5, A9; ::_thesis: verum
end;
supposeA10: y = {} ; ::_thesis: b1 in the topology of T
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 the topology of T by A7, A10, PRE_TOPC:def_1; ::_thesis: verum
end;
end;
end;
hence  FinMeetCl the topology of T c= the topology of T by SUBSET_1:2; ::_thesis: verum
end;

theorem Th6: :: CANTOR_1:6
for T being TopSpace holds the topology of T = UniCl the topology of T
proof
let T be TopSpace; ::_thesis: the topology of T = UniCl the topology of T
thus  the topology of T c= UniCl the topology of T by Th1; :: according to XBOOLE_0:def_10 ::_thesis: UniCl the topology of T c= the topology of T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in UniCl the topology of T or a in the topology of T )
assume A1: a in UniCl the topology of T ; ::_thesis: a in 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  a in the topology of T by PRE_TOPC:def_1; ::_thesis: verum
end;

theorem Th7: :: CANTOR_1:7
for T being non empty TopSpace holds the topology of T = UniCl (FinMeetCl the topology of T)
proof
let T be non empty TopSpace; ::_thesis: the topology of T = UniCl (FinMeetCl the topology of T)
 the topology of T = FinMeetCl the topology of T by Th5;
hence  the topology of T = UniCl (FinMeetCl the topology of T) by Th6; ::_thesis: verum
end;

theorem Th8: :: CANTOR_1:8
for X being set
for A being Subset-Family of X holds X in FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds X in FinMeetCl A
let A be Subset-Family of X; ::_thesis: X in FinMeetCl A
 {} 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  X in FinMeetCl A by A1, Def3; ::_thesis: verum
end;

theorem Th9: :: CANTOR_1:9
for X being set
for A, B being Subset-Family of X st A c= B holds
UniCl A c= UniCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds
UniCl A c= UniCl B
let A, B be Subset-Family of X; ::_thesis: ( A c= B implies UniCl A c= UniCl B )
assume A1: A c= B ; ::_thesis: UniCl A c= UniCl B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl A or x in UniCl B )
assume A2: x in UniCl A ; ::_thesis: x in UniCl B
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  x in UniCl B by A4, Def1; ::_thesis: verum
end;

theorem Th10: :: CANTOR_1:10
for X being set
for R being non empty Subset-Family of (bool X)
for F being Subset-Family of X st F =  {  (Intersect x) where x is Element of R : verum  }  holds
Intersect F = Intersect (union R)
proof
let X be set ; ::_thesis: for R being non empty Subset-Family of (bool X)
for F being Subset-Family of X st F =  {  (Intersect x) where x is Element of R : verum  }  holds
Intersect F = Intersect (union R)
let R be non empty Subset-Family of (bool X); ::_thesis: for F being Subset-Family of X st F =  {  (Intersect x) where x is Element of R : verum  }  holds
Intersect F = Intersect (union R)
let F be Subset-Family of X; ::_thesis: ( F =  {  (Intersect x) where x is Element of R : verum  }  implies Intersect F = Intersect (union R) )
assume A1: F =  {  (Intersect x) where x is Element of R : verum  }  ; ::_thesis: Intersect F = Intersect (union R)
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Intersect (union R) c= Intersect F
let c be set ; ::_thesis: ( c in Intersect F implies c in Intersect (union R) )
assume A2: c in Intersect F ; ::_thesis: c in Intersect (union R)
 for Y being set st Y in union R holds
c in Y
proof
let Y be set ; ::_thesis: ( Y in union R implies c in Y )
assume  Y in union R ; ::_thesis: c in Y
then consider d being set  such that
A3: Y in d and
A4: d in R by TARSKI:def_4;
reconsider d = d as Subset-Family of X by A4;
reconsider d = d as Subset-Family of X ;
 Intersect d in F by A1, A4;
then  c in Intersect d by A2, SETFAM_1:43;
hence  c in Y by A3, SETFAM_1:43; ::_thesis: verum
end;
hence  c in Intersect (union R) by A2, SETFAM_1:43; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Intersect (union R) or c in Intersect F )
assume A5: c in Intersect (union R) ; ::_thesis: c in Intersect F
 for Y being set st Y in F holds
c in Y
proof
let Y be set ; ::_thesis: ( Y in F implies c in Y )
assume  Y in F ; ::_thesis: c in Y
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  c in Y by A5, A6; ::_thesis: verum
end;
hence  c in Intersect F by A5, SETFAM_1:43; ::_thesis: verum
end;

theorem Th11: :: CANTOR_1:11
for X being set
for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
let A be Subset-Family of X; ::_thesis: FinMeetCl A = FinMeetCl (FinMeetCl A)
defpred S1[ 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; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl (FinMeetCl A) c= FinMeetCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl (FinMeetCl A) or x in FinMeetCl A )
assume A1: x in FinMeetCl (FinMeetCl A) ; ::_thesis: x in 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 holds
ex u being set st
( u in bool A & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in Y implies ex u being set st
( u in bool A & S1[e,u] ) )
assume A6: e in Y ; ::_thesis: ex u being set st
( u in bool A & S1[e,u] )
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 ; ::_thesis: ( Y in bool A & S1[e,Y] )
thus  ( Y in bool A & S1[e,Y] ) by A7; ::_thesis: verum
end;
consider f being Function of Y,(bool A) such that
A8: for e being set st e in Y holds
S1[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:  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  c= Y
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  or l in Y )
assume  l in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  ; ::_thesis: l in Y
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  S1[v,f . v] by A8;
hence  l in Y by A10, A12, A13, FUNCT_2:def_1; ::_thesis: verum
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 = y as Subset-Family of X ;
 Y c=  {  (Intersect s) where s is Subset-Family of X : s in rng f  }
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in Y or l in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  )
assume A15: l in Y ; ::_thesis: l in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }
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  l in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  by A16; ::_thesis: verum
end;
then A18: Y =  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  by A9, XBOOLE_0:def_10;
A19: x = Intersect y
proof
percases ( rng f <> {} or rng f = {} ) ;
supposeA20: rng f <> {} ; ::_thesis: x = Intersect y
 ( 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 = GGG as non empty Subset-Family of (bool X) ;
  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  =  {  (Intersect b) where b is Element of GGG : verum  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (Intersect b) where b is Element of GGG : verum  }  c=  {  (Intersect s) where s is Subset-Family of X : s in rng f  }
let x be set ; ::_thesis: ( x in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  implies x in  {  (Intersect b) where b is Element of GGG : verum  }  )
assume  x in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  ; ::_thesis: x in  {  (Intersect b) where b is Element of GGG : verum  }
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 : verum  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Intersect b) where b is Element of GGG : verum  }  or x in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  )
assume  x in  {  (Intersect b) where b is Element of GGG : verum  }  ; ::_thesis: x in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }
then  ex s being Element of GGG st x = Intersect s ;
hence  x in  {  (Intersect s) where s is Subset-Family of X : s in rng f  }  ; ::_thesis: verum
end;
hence  x = Intersect y by A4, A18, Th10; ::_thesis: verum
end;
supposeA21: rng f = {} ; ::_thesis: x = Intersect y
 Y = dom f by FUNCT_2:def_1;
hence  x = Intersect y by A4, A21, RELAT_1:38, RELAT_1:41, ZFMISC_1:2; ::_thesis: verum
end;
end;
end;
 for V being set st V in rng f holds
V is finite
proof
let V be set ; ::_thesis: ( V in rng f implies V is finite )
assume  V in rng f ; ::_thesis: V is finite
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 = x as Subset of X ;
reconsider G = f . x as Subset-Family of X ;
 x in Y by A22, FUNCT_2:def_1;
then  S1[x,G] by A8;
hence  V is finite by A23; ::_thesis: verum
end;
then  union (rng f) is finite by A3, FINSET_1:7;
hence  x in FinMeetCl A by A14, A19, Def3; ::_thesis: verum
end;

theorem :: CANTOR_1:12
for X being set
for A being Subset-Family of X
for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X
for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let A be Subset-Family of X; ::_thesis: for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let a, b be set ; ::_thesis: ( a in FinMeetCl A & b in FinMeetCl A implies a /\ b in FinMeetCl A )
assume A1: ( a in FinMeetCl A & b in FinMeetCl A ) ; ::_thesis: a /\ b in FinMeetCl A
then reconsider M = {a,b} as Subset-Family of X by ZFMISC_1:32;
reconsider M = 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  a /\ b in FinMeetCl A by A2, Th11; ::_thesis: verum
end;

theorem Th13: :: CANTOR_1:13
for X being set
for A being Subset-Family of X
for 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 ; ::_thesis: for A being Subset-Family of X
for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let A be Subset-Family of X; ::_thesis: for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let a, b be set ; ::_thesis: ( a c= FinMeetCl A & b c= FinMeetCl A implies INTERSECTION (a,b) c= FinMeetCl A )
assume A1: ( a c= FinMeetCl A & b c= FinMeetCl A ) ; ::_thesis: INTERSECTION (a,b) c= FinMeetCl A
let Z be set ; :: according to TARSKI:def_3 ::_thesis: ( not Z in INTERSECTION (a,b) or Z in FinMeetCl A )
assume  Z in INTERSECTION (a,b) ; ::_thesis: Z in FinMeetCl A
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 = 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  Z in FinMeetCl A by A3, A4, Th11; ::_thesis: verum
end;

theorem Th14: :: CANTOR_1:14
for X being set
for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B
let A, B be Subset-Family of X; ::_thesis: ( A c= B implies FinMeetCl A c= FinMeetCl B )
assume A1: A c= B ; ::_thesis: FinMeetCl A c= FinMeetCl B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl A or x in FinMeetCl B )
assume A2: x in FinMeetCl A ; ::_thesis: x in FinMeetCl B
then reconsider x = 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  x in FinMeetCl B by A4, Def3; ::_thesis: verum
end;

registration
let X be set ;
let A be Subset-Family of X;
cluster FinMeetCl A ->  non empty ;
coherence
 not FinMeetCl A is empty by Th8;
end;

theorem Th15: :: CANTOR_1:15
for X being non empty set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof
let X be non empty set ; ::_thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
A1: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A by Th8;
now__::_thesis:_ex_Y_being_Subset-Family_of_X_st_
(_Y_c=_FinMeetCl_A_&_[#]_TopStruct(#_X,(UniCl_(FinMeetCl_A))_#)_=_union_Y_)
reconsider Y = {([#] TopStruct(# X,(UniCl (FinMeetCl A)) #))} as Subset-Family of X by ZFMISC_1:68;
reconsider Y = Y as Subset-Family of X ;
take Y = Y; ::_thesis: ( Y c= FinMeetCl A & [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y )
thus  Y c= FinMeetCl A by A1, ZFMISC_1:31; ::_thesis: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y
thus  [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y by ZFMISC_1:25; ::_thesis: verum
end;
hence  the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Def1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) )
thus  for a being Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) st a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ::_thesis: for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
proof
let a be Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume A2: a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
defpred S1[ set ] means  ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) 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 S1[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  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }  c= a
let x be set ; ::_thesis: ( x in a implies x in  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }  )
assume A5: x in a ; ::_thesis: x in  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }
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  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }  by A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }  or x in a )
assume  x in  {  (union B) where B is Subset of (FinMeetCl A) : B in b  }  ; ::_thesis: x in a
then consider B being Subset of (FinMeetCl A) such that
A8: x = union B and
A9: B in b ;
 ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st
( c in a & c = union B ) by A3, A9;
hence  x in a by A8; ::_thesis: verum
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  union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A4, Def1; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( not a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume  a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: ( not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
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 TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
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  a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A15, A14, Def1; ::_thesis: verum
end;

definition
let X be TopStruct ;
let F be Subset-Family of X;
attrF is quasi_prebasis  means :Def4: :: CANTOR_1:def 4
 ex G being Basis of X st G c= FinMeetCl F;
end;

:: deftheorem Def4 defines quasi_prebasis CANTOR_1:def_4_:_
 for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_prebasis iff ex G being Basis of X st G c= FinMeetCl F );

registration
let X be TopStruct ;
cluster the topology of X ->  quasi_prebasis ;
coherence
 the topology of X is quasi_prebasis
proof
take  the topology of X ; :: according to CANTOR_1:def_4 ::_thesis: the topology of X c= FinMeetCl the topology of X
thus  the topology of X c= FinMeetCl the topology of X by Th4; ::_thesis: verum
end;
cluster open quasi_basis  ->  quasi_prebasis for Element of bool (bool the carrier of X);
coherence
 for b1 being Basis of X holds b1 is quasi_prebasis
proof
let F be Basis of X; ::_thesis: F is quasi_prebasis
take  F ; :: according to CANTOR_1:def_4 ::_thesis: F c= FinMeetCl F
thus  F c= FinMeetCl F by Th4; ::_thesis: verum
end;
cluster open quasi_prebasis for Element of bool (bool the carrier of X);
existence
 ex b1 being Subset-Family of X st
( b1 is open & b1 is quasi_prebasis )
proof
take  the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_prebasis )
thus  ( the topology of X is open & the topology of X is quasi_prebasis ) ; ::_thesis: verum
end;
end;

definition
let X be TopStruct ;
mode prebasis of X is open quasi_prebasis Subset-Family of X;
end;

theorem Th16: :: CANTOR_1:16
for X being non empty set
for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)
proof
let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)
let Y be Subset-Family of X; ::_thesis: Y is Basis of TopStruct(# X,(UniCl Y) #)
 Y c= UniCl Y by Th1;
hence  Y is Basis of TopStruct(# X,(UniCl Y) #) by Def2, TOPS_2:64; ::_thesis: verum
end;

theorem Th17: :: CANTOR_1:17
for T1, T2 being non empty strict TopSpace
for 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 non empty strict TopSpace; ::_thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
T1 = T2
let P be prebasis of T1; ::_thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies T1 = T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2 ; ::_thesis: T1 = 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  T1 = T2 by A1, A7, A11, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th18: :: CANTOR_1:18
for X being non empty set
for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
proof
let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
let A be Subset-Family of X; ::_thesis: A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #)
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
reconsider A9 = A as Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) ;
now__::_thesis:_(_A9_is_open_&_A9_is_quasi_prebasis_)
 ( A9 c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4;
then  A9 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by XBOOLE_1:1;
hence  A9 is open by TOPS_2:64; ::_thesis: A9 is quasi_prebasis
thus  A9 is quasi_prebasis ::_thesis: verum
proof
reconsider B = FinMeetCl A9 as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th16;
take  B ; :: according to CANTOR_1:def_4 ::_thesis: B c= FinMeetCl A9
thus  B c= FinMeetCl A9 ; ::_thesis: verum
end;
end;
hence  A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum
end;

definition
func the_Cantor_set  ->  non empty strict TopSpace means :: CANTOR_1:def 5
( 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
 ex b1 being non empty strict TopSpace st
( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 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 ) ) )
proof
defpred S1[ 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 S1[y] ) from SUBSET_1:sch_3();
reconsider T = TopStruct(# (product (NAT --> {0,1})),(UniCl (FinMeetCl Y)) #) as non empty strict TopSpace by Th15;
take  T ; ::_thesis: ( the carrier of T = product (NAT --> {0,1}) & ex P being prebasis of T 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 ) ) )
thus  the carrier of T = product (NAT --> {0,1}) ; ::_thesis: ex P being prebasis of T 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 ) )
reconsider Y = Y as prebasis of T by Th18;
take  Y ; ::_thesis: for X being Subset of (product (NAT --> {0,1})) holds
( X in Y iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) )
thus  for X being Subset of (product (NAT --> {0,1})) holds
( X in Y 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 A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict TopSpace st the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 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 ) ) & the carrier of b2 = product (NAT --> {0,1}) & ex P being prebasis of b2 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 ) ) holds
b1 = b2
proof
let T1, T2 be non empty strict TopSpace; ::_thesis: ( the carrier of T1 = product (NAT --> {0,1}) & 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 ) ) & the carrier of T2 = product (NAT --> {0,1}) & 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 ) ) implies T1 = T2 )
assume 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 ) ) ; ::_thesis: T1 = T2
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__::_thesis:_for_x_being_Subset_of_(product_(NAT_-->_{0,1}))_holds_
(_x_in_P1_iff_x_in_P2_)
let x be Subset of (product (NAT --> {0,1})); ::_thesis: ( x in P1 iff x in P2 )
 ( 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; ::_thesis: verum
end;
then  P1 = P2 by A2, A4, SUBSET_1:3;
hence  T1 = T2 by A2, A4, Th17; ::_thesis: verum
end;
end;

:: deftheorem  defines the_Cantor_set CANTOR_1:def_5_:_
 for b1 being non empty strict TopSpace holds
( b1 = the_Cantor_set iff ( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 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 ) ) ) );