:: The Cantor Set
:: by Alexander Yu. Shibakov and Andrzej Trybulec
::
:: Received January 9, 1995
:: Copyright (c) 1995-2026 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, ORDINAL1, NUMBERS, 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, XBOOLE_0;
equalities STRUCT_0;
expansions TARSKI, XBOOLE_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 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 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 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
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 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 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;
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 object;
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;
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 object;
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;
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 = the set of all
Intersect x where x is 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 is Element of R;
hereby
let c be object;
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 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 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[object,object] means
ex A being 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 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 object st e in Y ex u being 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 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 object 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 object;
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 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 being 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 is Element of GGG
proof
hereby
let x be object;
assume x in fz;
then ex s being Subset-Family of X st x = Intersect s & s in rng f;
hence
x in the set of all Intersect b where b is Element of GGG;
end;
let x be object;
assume
x in the set of all Intersect b where b is Element of GGG;
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 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
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 object;
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 object;
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;
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 object;
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 object;
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
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 Th16:
for X being non empty set, Y being Subset-Family of X holds
Y is Basis of TopStruct (#X, UniCl Y#) by Def2,Th1,TOPS_2:64;
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;
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;
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 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;
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