Copyright (c) 2003 Association of Mizar Users
environ
vocabulary BOOLE, KURATO_1, FINSET_1, TOPS_1, PRE_TOPC, CARD_1, SUBSET_1,
RCOMP_1, PROB_1, INCPROJ, SETFAM_1, AMI_1, TOPMETR, RAT_1, BORSUK_5;
notation XBOOLE_0, TARSKI, SUBSET_1, STRUCT_0, NUMBERS, XREAL_0, PRE_TOPC,
TOPS_1, ENUMSET1, CARD_1, FINSET_1, RCOMP_1, INCPROJ, NAT_1, SEQ_4,
RCOMP_2, PCOMPS_1, TOPMETR, AMI_1, BORSUK_5;
constructors TOPS_1, NAT_1, INCPROJ, RCOMP_2, PSCOMP_1, INTEGRA1, COMPTS_1,
LIMFUNC1, TOPGRP_1, TREAL_1, DOMAIN_1, RAT_1, PROB_1, AMI_1, BORSUK_5,
MEMBERED;
clusters FINSET_1, TOPS_1, TOPREAL6, AMI_1, XBOOLE_0, BORSUK_5, MEMBERED,
ZFMISC_1;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
definitions XBOOLE_0, TARSKI, INCPROJ, AMI_1, BORSUK_5;
theorems ENUMSET1, TOPS_1, PRE_TOPC, CARD_2, REAL_1, AXIOMS, XBOOLE_0,
TDLAT_1, TARSKI, TOPMETR, ZFMISC_1, XBOOLE_1, JORDAN6, SETFAM_1,
WAYBEL12, AMI_1, MEASURE1, BORSUK_5;
begin :: Fourteen Kuratowski Sets
reserve T for non empty TopSpace;
reserve A for Subset of T;
theorem Th1:
Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)`
proof
set B = Cl (Cl A)`;
Int B c= B by TOPS_1:44;
then Cl Int B c= Cl B by PRE_TOPC:49;
then A1: Cl Int B c= B by PRE_TOPC:52;
set U = (Cl A)`;
A2: U c= Cl U by PRE_TOPC:48;
U = Int U by TOPS_1:55;
then U c= Int Cl U by A2,TOPS_1:48;
then Cl U c= Cl Int Cl U by PRE_TOPC:49;
then Cl Int B = B by A1,XBOOLE_0:def 10;
hence thesis by TOPS_1:def 1;
end;
Lm1:
for T being 1-sorted,
A, B being Subset-Family of T holds
A \/ B is Subset-Family of T;
definition let T, A;
func Kurat14Part A equals :Def1:
{ A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` };
coherence;
end;
definition let T, A;
cluster Kurat14Part A -> finite;
coherence
proof
Kurat14Part A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by Def1;
hence thesis;
end;
end;
definition let T, A;
func Kurat14Set A -> Subset-Family of T equals :Def2:
{ A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
coherence
proof
set X1 = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` },
X2 = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
X1 c= bool the carrier of T
proof
let x be set;
assume x in X1;
then x = A or x = Cl A or x = (Cl A)` or x = Cl (Cl A)`
or x = (Cl (Cl A)`)` or
x = Cl (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` by ENUMSET1:33;
hence thesis;
end;
then reconsider X1 as Subset-Family of T by SETFAM_1:def 7;
X2 c= bool the carrier of T
proof
let x be set;
assume x in X2;
then x = A` or x = Cl A` or x = (Cl A`)` or x = Cl (Cl A`)` or
x = (Cl (Cl A`)`)` or
x = Cl (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)` by ENUMSET1:33;
hence thesis;
end;
then reconsider X2 as Subset-Family of T by SETFAM_1:def 7;
X1 \/ X2 is Subset-Family of T;
hence thesis;
end;
end;
theorem Th2:
Kurat14Set A = Kurat14Part A \/ Kurat14Part A`
proof
Kurat14Set A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def2
.= Kurat14Part A \/ { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def1;
hence thesis by Def1;
end;
theorem Th3:
A in Kurat14Set A & Cl A in Kurat14Set A & (Cl A)` in Kurat14Set A &
Cl (Cl A)` in Kurat14Set A & (Cl (Cl A)`)` in Kurat14Set A &
Cl (Cl (Cl A)`)` in Kurat14Set A & (Cl (Cl (Cl A)`)`)` in Kurat14Set A
proof
Kurat14Set A = Kurat14Part A \/ Kurat14Part A` by Th2;
then A1: Kurat14Part A c= Kurat14Set A by XBOOLE_1:7;
Kurat14Part A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by Def1;
then A in Kurat14Part A & Cl A in Kurat14Part A &
(Cl A)` in Kurat14Part A &
Cl (Cl A)` in Kurat14Part A & (Cl (Cl A)`)` in Kurat14Part A &
Cl (Cl (Cl A)`)` in Kurat14Part A & (Cl (Cl (Cl A)`)`)` in Kurat14Part A
by ENUMSET1:34;
hence thesis by A1;
end;
theorem Th4:
A` in Kurat14Set A & Cl A` in Kurat14Set A &
(Cl A`)` in Kurat14Set A & Cl (Cl A`)` in Kurat14Set A &
(Cl (Cl A`)`)` in Kurat14Set A & Cl (Cl (Cl A`)`)` in Kurat14Set A &
(Cl (Cl (Cl A`)`)`)` in Kurat14Set A
proof
Kurat14Set A = Kurat14Part A \/ Kurat14Part A` by Th2;
then A1: Kurat14Part A` c= Kurat14Set A by XBOOLE_1:7;
Kurat14Part A` = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def1;
then A` in Kurat14Part A` & Cl A` in Kurat14Part A` &
(Cl A`)` in Kurat14Part A` &
Cl (Cl A`)` in Kurat14Part A` & (Cl (Cl A`)`)` in Kurat14Part A` &
Cl (Cl (Cl A`)`)` in Kurat14Part A` &
(Cl (Cl (Cl A`)`)`)` in Kurat14Part A`
by ENUMSET1:34;
hence thesis by A1;
end;
definition let T, A;
func Kurat14ClPart A -> Subset-Family of T equals :Def3:
{ Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` };
coherence
proof
A1: {Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)`}
=
{ Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } \/ { Cl A`, Cl (Cl A`)`,
Cl (Cl (Cl A`)`)` } by ENUMSET1:53;
A2: { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)` } is Subset-Family of T
by BORSUK_5:32;
{ Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } is Subset-Family of T
by BORSUK_5:32;
hence thesis by A1,A2,Lm1;
end;
func Kurat14OpPart A -> Subset-Family of T equals :Def4:
{ (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
coherence
proof
A3: { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } =
{ (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by ENUMSET1:53;
A4: { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } is Subset-Family of T
by BORSUK_5:32;
{ (Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } is Subset-Family of T
by BORSUK_5:32;
hence thesis by A3,A4,Lm1;
end;
end;
Lm2:
Kurat14Set A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } \/
{ A, A` } \/
{ (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` }
proof
A1: Kurat14Set A = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)` ,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def2;
set Y1 = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` },
Y2 = { A, A` },
Y3 = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
set Y = Y1 \/ Y2 \/ Y3;
A2: Y3 c= Y & Y1 \/ Y2 c= Y by XBOOLE_1:7;
Y1 c= Y1 \/ Y2 & Y2 c= Y1 \/ Y2 by XBOOLE_1:7;
then A3: Y1 c= Y & Y2 c= Y by A2,XBOOLE_1:1;
A4: Cl A in Y1 & Cl (Cl A)` in Y1 & Cl (Cl (Cl A)`)` in Y1 &
Cl A` in Y1 & Cl (Cl A`)` in Y1 & Cl (Cl (Cl A`)`)` in Y1 by ENUMSET1:29;
A5: A in Y2 & A` in Y2 by TARSKI:def 2;
(Cl A)` in Y3 & (Cl (Cl A)`)` in Y3 & (Cl (Cl (Cl A)`)`)` in Y3 &
(Cl A`)` in Y3 & (Cl (Cl A`)`)` in Y3 & (Cl (Cl (Cl A`)`)`)` in Y3
by ENUMSET1:29;
then A6: Cl A in Y & Cl (Cl A)` in Y & Cl (Cl (Cl A)`)` in Y &
Cl A` in Y & Cl (Cl A`)` in Y & Cl (Cl (Cl A`)`)` in Y &
A in Y & A` in Y &
(Cl A)` in Y & (Cl (Cl A)`)` in Y & (Cl (Cl (Cl A)`)`)` in Y &
(Cl A`)` in Y & (Cl (Cl A`)`)` in Y & (Cl (Cl (Cl A`)`)`)` in Y
by A2,A3,A4,A5;
Kurat14Set A = Y
proof
thus Kurat14Set A c= Y
proof
let x be set;
assume
A7: x in Kurat14Set A;
per cases by A1,A7,XBOOLE_0:def 2;
suppose x in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` };
hence thesis by A6,ENUMSET1:33;
suppose x in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
hence thesis by A6,ENUMSET1:33;
end;
thus Y c= Kurat14Set A
proof
let x be set;
assume x in Y;
then A8: x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } \/ { A, A` } or
x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
per cases by A8,XBOOLE_0:def 2;
suppose x in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` };
then x = Cl A or x = Cl (Cl A)` or x = Cl (Cl (Cl A)`)` or
x = Cl A` or x = Cl (Cl A`)` or x = Cl (Cl (Cl A`)`)` by ENUMSET1:28;
hence thesis by Th3,Th4;
suppose x in { A, A` };
then x = A or x = A` by TARSKI:def 2;
hence thesis by Th3,Th4;
suppose x in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
then x = (Cl A)` or x = (Cl (Cl A)`)` or x = (Cl (Cl (Cl A)`)`)` or
x = (Cl A`)` or x = (Cl (Cl A`)`)` or x = (Cl (Cl (Cl A`)`)`)`
by ENUMSET1:28;
hence thesis by Th3,Th4;
end;
end;
hence thesis;
end;
theorem Th5:
Kurat14Set A = { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A
proof
Kurat14Set A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } \/
{ A, A` } \/
{ (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Lm2
.= { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } \/
{ A, A` } \/ Kurat14OpPart A by Def4
.= { A, A` } \/ Kurat14ClPart A \/ Kurat14OpPart A by Def3;
hence thesis;
end;
definition let T, A;
cluster Kurat14Set A -> finite;
coherence
proof
set X = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` },
Y = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
X \/ Y is finite;
hence thesis by Def2;
end;
end;
theorem Th6:
for Q being Subset of T holds
Q in Kurat14Set A implies Q` in Kurat14Set A & Cl Q in Kurat14Set A
proof
let Q be Subset of T;
set k1 = Cl A, k2 = (Cl A)`, k3 = Cl (Cl A)`,
k4 = (Cl (Cl A)`)`, k5 = Cl (Cl (Cl A)`)`, k6 = (Cl (Cl (Cl A)`)`)`,
k7 = Cl A`, k8 = (Cl A`)`, k9 = Cl (Cl A`)`,
k10 = (Cl (Cl A`)`)`, k11 = Cl (Cl (Cl A`)`)`,
k12 = (Cl (Cl (Cl A`)`)`)`;
assume Q in Kurat14Set A;
then A1: Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by Def2;
per cases by A1,XBOOLE_0:def 2;
suppose
A2: Q in { A, k1, k2, k3, k4, k5, k6 };
Q` in Kurat14Set A & Cl Q in Kurat14Set A
proof
per cases by A2,ENUMSET1:33;
suppose
A3: Q = A;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A4: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` in { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by A3,ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A4,Def2;
suppose
A5: Q = Cl A;
then Cl Q = Cl A by TOPS_1:26;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A6: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` in { A, k1, k2, k3, k4, k5, k6 } by A5,ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A6,Def2;
suppose
A7: Q = (Cl A)`;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A8: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` = Cl A by A7;
then Q` in { A, Cl A, (Cl A)`, k3, k4, k5, k6 } by ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A8,Def2;
suppose
A9: Q = Cl (Cl A)`;
then Cl Q = Cl (Cl A)` by TOPS_1:26;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A10: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` in { A, k1, k2, k3, k4, k5, k6 } by A9,ENUMSET1:34;
then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A10,Def2;
suppose
A11: Q = (Cl (Cl A)`)`;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A12: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` = Cl (Cl A)` by A11;
then Q` in { A, k1, k2, Cl (Cl A)`, k4, k5, k6 } by ENUMSET1:34;
then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A12,Def2;
suppose
A13: Q = Cl (Cl (Cl A)`)`;
then Cl Q = Cl (Cl (Cl A)`)` by TOPS_1:26;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by ENUMSET1:34;
then A14: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` in { A, k1, k2, k3, k4, k5, k6 } by A13,ENUMSET1:34;
then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A14,Def2;
suppose
A15: Q = (Cl (Cl (Cl A)`)`)`;
Cl (Cl (Cl (Cl A)`)`)` = Cl (Cl A)` by Th1;
then Cl Q in { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` } by A15,ENUMSET1:34;
then A16: Cl Q in { A, Cl A, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` = Cl (Cl (Cl A)`)` by A15;
then Q` in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A16,Def2;
end;
hence thesis;
suppose
A17:Q in { A`, k7, k8, k9, k10, k11, k12 };
Q` in Kurat14Set A & Cl Q in Kurat14Set A
proof
per cases by A17,ENUMSET1:33;
suppose
A18: Q = A`;
then Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12 } by ENUMSET1:34;
then A19: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by XBOOLE_0:def 2;
Q` = A by A18;
then Q` in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A19,Def2;
suppose
A20: Q = Cl A`;
then Cl Q = Cl A` by TOPS_1:26;
then Cl Q in { A`, Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A21: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` in { A`, k7, (Cl A`)`, k9, k10, k11, k12} by A20,ENUMSET1:34;
then Q` in { A, k1, k2, k3, (Cl (Cl A)`)`, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A21,Def2;
suppose
A22: Q = (Cl A`)`;
then Cl Q in { A`, k7, k8, Cl (Cl A`)`, k10, k11, k12} by ENUMSET1:34;
then A23: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` = Cl A` by A22;
then Q` in { A`, Cl A`, k8, k9, k10, k11, k12} by ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A23,Def2;
suppose
A24: Q = Cl (Cl A`)`;
then Cl Q = Cl (Cl A`)` by TOPS_1:26;
then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A25: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` in { A`, k7, k8, k9, k10, k11, k12} by A24,ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A25,Def2;
suppose
A26: Q = (Cl (Cl A`)`)`;
then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A27: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` = Cl (Cl A`)` by A26;
then Q` in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A27,Def2;
suppose
A28: Q = Cl (Cl (Cl A`)`)`;
then Cl Q = Cl (Cl (Cl A`)`)` by TOPS_1:26;
then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A29: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` in { A`, k7, k8, k9, k10, k11, k12} by A28,ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A29,Def2;
suppose
A30: Q = (Cl (Cl (Cl A`)`)`)`;
then Cl Q = Cl (Cl A`)` by Th1;
then Cl Q in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then A31: Cl Q in { A, k1, k2, k3, k4, k5, k6 } \/
{ A`, Cl A`, k8, k9, k10, k11, k12} by XBOOLE_0:def 2;
Q` = Cl (Cl (Cl A`)`)` by A30;
then Q` in { A`, k7, k8, k9, k10, k11, k12} by ENUMSET1:34;
then Q` in { A, k1, k2, k3, k4, k5 , k6 } \/
{ A`, k7, k8, k9, k10, k11, k12 } by XBOOLE_0:def 2;
hence thesis by A31,Def2;
end;
hence thesis;
end;
theorem
card Kurat14Set A <= 14
proof
set X = { A, Cl A, (Cl A)`, Cl (Cl A)`, (Cl (Cl A)`)`,
Cl (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)` },
Y = { A`, Cl A`, (Cl A`)`, Cl (Cl A`)`, (Cl (Cl A`)`)`,
Cl (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` };
A1: card (X \/ Y) <= card X + card Y by CARD_2:62;
card X <= 7 & card Y <= 7 by CARD_2:74;
then card X + card Y <= 7 + 7 by REAL_1:55;
then card (X \/ Y) <= 14 by A1,AXIOMS:22;
hence thesis by Def2;
end;
begin :: Seven Kuratowski Sets
definition let T, A;
func Kurat7Set A -> Subset-Family of T equals :Def5:
{ A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
coherence
proof
set X = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
X c= bool the carrier of T
proof
let x be set;
assume x in X;
then x = A or x = Int A or x = Cl A or x = Int Cl A or x = Cl Int A
or x = Cl Int Cl A or x = Int Cl Int A by ENUMSET1:33;
hence thesis;
end;
then X is Subset-Family of T by SETFAM_1:def 7;
hence thesis;
end;
end;
theorem Th8:
A in Kurat7Set A & Int A in Kurat7Set A &
Cl A in Kurat7Set A & Int Cl A in Kurat7Set A & Cl Int A in Kurat7Set A &
Cl Int Cl A in Kurat7Set A & Int Cl Int A in Kurat7Set A
proof
Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
Int Cl Int A } by Def5;
hence thesis by ENUMSET1:34;
end;
theorem
Kurat7Set A = { A } \/ { Int A, Int Cl A, Int Cl Int A } \/
{ Cl A, Cl Int A, Cl Int Cl A }
proof
Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
Int Cl Int A } by Def5
.= { A } \/ { Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
Int Cl Int A } by ENUMSET1:56
.= { A } \/ ({ Int A, Int Cl A, Int Cl Int A } \/
{ Cl A, Cl Int A, Cl Int Cl A }) by BORSUK_5:3
.= { A } \/ { Int A, Int Cl A, Int Cl Int A } \/
{ Cl A, Cl Int A, Cl Int Cl A } by XBOOLE_1:4;
hence thesis;
end;
definition let T, A;
cluster Kurat7Set A -> finite;
coherence
proof
set X = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A };
X is finite;
hence thesis by Def5;
end;
end;
theorem Th10:
for Q being Subset of T holds
Q in Kurat7Set A implies Int Q in Kurat7Set A & Cl Q in Kurat7Set A
proof
let Q be Subset of T;
set k1 = Int A, k2 = Cl A, k3 = Int Cl A,
k4 = Cl Int A, k5 = Cl Int Cl A, k6 = Int Cl Int A;
assume Q in Kurat7Set A;
then A1: Q in { A, k1, k2, k3, k4, k5, k6} by Def5;
Int Q in Kurat7Set A & Cl Q in Kurat7Set A
proof
per cases by A1,ENUMSET1:33;
suppose
A2: Q = A;
then A3: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q in { A, k1, k2, k3, k4, k5, k6 } by A2,ENUMSET1:34;
hence thesis by A3,Def5;
suppose
A4: Q = Int A;
then A5: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q = Int A by A4,TOPS_1:45;
then Int Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
hence thesis by A5,Def5;
suppose
A6: Q = Cl A;
then Cl Q = Cl A by TOPS_1:26;
then A7: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q in { A, k1, k2, k3, k4, k5, k6 } by A6,ENUMSET1:34;
hence thesis by A7,Def5;
suppose
A8: Q = Int Cl A;
then A9: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q = Int Cl A by A8,TOPS_1:45;
then Int Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
hence thesis by A9,Def5;
suppose
A10: Q = Cl Int A;
then Cl Q = Cl Int A by TOPS_1:26;
then A11: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q in { A, k1, k2, k3, k4, k5, k6 } by A10,ENUMSET1:34;
hence thesis by A11,Def5;
suppose
A12: Q = Cl Int Cl A;
then Cl Q = Cl Int Cl A by TOPS_1:26;
then A13: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Cl Int Cl A = Int Cl A by TDLAT_1:5;
then Int Q in { A, k1, k2, k3, k4, k5, k6 } by A12,ENUMSET1:34;
hence thesis by A13,Def5;
suppose
A14: Q = Int Cl Int A;
then Cl Q = Cl Int A by TOPS_1:58;
then A15: Cl Q in { A, k1, k2, k3, k4, k5, k6 } by ENUMSET1:34;
Int Q = Int Cl Int A by A14,TOPS_1:45;
then Int Q in { A, k1, k2, k3, k4, k5, k6} by ENUMSET1:34;
hence thesis by A15,Def5;
end;
hence thesis;
end;
theorem
card Kurat7Set A <= 7
proof
Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A,
Cl Int Cl A, Int Cl Int A } by Def5;
hence thesis by CARD_2:74;
end;
begin :: The Set Generating Exactly Fourteen Kuratowski Sets
definition
func KurExSet -> Subset of R^1 equals :Def6:
{1} \/ RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[;
coherence by TOPMETR:24;
end;
theorem Th12:
Cl KurExSet = {1} \/ [. 2,+infty.[
proof
reconsider B = {1},
C = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ as Subset of R^1
by TOPMETR:24;
set A = KurExSet;
A = {1} \/ (RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[)
by Def6,XBOOLE_1:113;
then A1: Cl A = Cl B \/ Cl C by PRE_TOPC:50;
Cl B = {1} by BORSUK_5:61;
hence Cl A = {1} \/ [. 2,+infty.[ by A1,BORSUK_5:82;
end;
theorem Th13:
(Cl KurExSet)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
theorem Th14:
Cl (Cl KurExSet)` = ].-infty, 2 .] by Th13,BORSUK_5:96;
theorem Th15:
(Cl (Cl KurExSet)`)` = ]. 2,+infty.[ by Th14,BORSUK_5:98;
theorem Th16:
Cl (Cl (Cl KurExSet)`)` = [. 2,+infty.[ by Th15,BORSUK_5:75;
theorem Th17:
(Cl (Cl (Cl KurExSet)`)`)` = ].-infty, 2 .[ by Th16,BORSUK_5:99;
theorem Th18:
KurExSet` = ].-infty, 1 .[ \/ ]. 1, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4}
proof
reconsider B = {1},
C = RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[ as Subset of R^1
by TOPMETR:24;
set A = KurExSet;
A1: A = {1} \/ (RAT (2,3) \/ ]. 3, 4 .[ \/ ]. 4,+infty.[)
by Def6,XBOOLE_1:113;
A2: B` = ].-infty, 1 .[ \/ ]. 1,+infty.[ by BORSUK_5:90;
C` = ].-infty, 2 .] \/ IRRAT(2,3) \/ {3} \/ {4} by BORSUK_5:89;
hence thesis by A1,A2,BORSUK_5:92,WAYBEL12:5;
end;
theorem Th19:
Cl KurExSet` = ].-infty, 3 .] \/ {4} by Th18,BORSUK_5:101;
theorem Th20:
(Cl KurExSet`)` = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th19,BORSUK_5:102;
theorem Th21:
Cl (Cl KurExSet`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;
theorem Th22:
(Cl (Cl KurExSet`)`)` = ].-infty, 3 .[ by Th21,BORSUK_5:99;
theorem Th23:
Cl (Cl (Cl KurExSet`)`)` = ].-infty, 3 .] by Th22,BORSUK_5:77;
theorem Th24:
(Cl (Cl (Cl KurExSet`)`)`)` = ]. 3,+infty.[ by Th23,BORSUK_5:98;
begin :: The Set Generating Exactly Seven Kuratowski Sets
theorem Th25:
Int KurExSet = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
theorem Th26:
Cl Int KurExSet = [. 3,+infty.[
proof
set A = KurExSet;
Cl (Cl A`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;
hence thesis by TOPS_1:def 1;
end;
theorem Th27:
Int Cl Int KurExSet = ]. 3,+infty.[
proof
set A = KurExSet;
(Cl (Cl A`)`)` = ].-infty, 3 .[ by Th21,BORSUK_5:99;
then A1: Cl (Cl (Cl A`)`)` = ].-infty, 3 .] by BORSUK_5:77;
Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
then Int Cl Int A = (Cl (Cl (Cl A`)`)`)` by TOPS_1:def 1;
hence thesis by A1,BORSUK_5:98;
end;
theorem Th28:
Int Cl KurExSet = ]. 2,+infty.[
proof
set A = KurExSet;
(Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
then Cl (Cl A)` = ].-infty, 2 .] by BORSUK_5:96;
then (Cl (Cl A)`)` = ]. 2,+infty.[ by BORSUK_5:98;
hence thesis by TOPS_1:def 1;
end;
theorem Th29:
Cl Int Cl KurExSet = [. 2,+infty.[
proof
set A = KurExSet;
(Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
then Cl (Cl A)` = ].-infty, 2 .] by BORSUK_5:96;
then (Cl (Cl A)`)` = ]. 2,+infty.[ by BORSUK_5:98;
then Cl (Cl (Cl A)`)` = [. 2,+infty.[ by BORSUK_5:75;
hence thesis by TOPS_1:def 1;
end;
begin :: The Difference Between Chosen Kuratowski Sets
theorem
Cl Int Cl KurExSet <> Int Cl KurExSet
proof
set A = KurExSet;
2 in Cl Int Cl A by Th29,BORSUK_5:15;
hence thesis by Th28,BORSUK_5:14;
end;
theorem Th31:
Cl Int Cl KurExSet <> Cl KurExSet
proof
set A = KurExSet;
1 in {1} by TARSKI:def 1;
then 1 in Cl A by Th12,XBOOLE_0:def 2;
hence thesis by Th29,BORSUK_5:15;
end;
theorem
Cl Int Cl KurExSet <> Int Cl Int KurExSet
proof
set A = KurExSet;
3 in Cl Int Cl A by Th29,BORSUK_5:15;
hence thesis by Th27,BORSUK_5:14;
end;
theorem Th33:
Cl Int Cl KurExSet <> Cl Int KurExSet
proof
set A = KurExSet;
2 in Cl Int Cl A by Th29,BORSUK_5:15;
hence Cl Int Cl A <> Cl Int A by Th26,BORSUK_5:15;
end;
theorem
Cl Int Cl KurExSet <> Int KurExSet
proof
set A = KurExSet;
A1: 2 in Cl Int Cl A by Th29,BORSUK_5:15;
Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence thesis by A1,BORSUK_5:86;
end;
theorem
Int Cl KurExSet <> Cl KurExSet
proof
set A = KurExSet;
1 in {1} by TARSKI:def 1;
then 1 in Cl A by Th12,XBOOLE_0:def 2;
hence thesis by Th28,BORSUK_5:14;
end;
theorem
Int Cl KurExSet <> Int Cl Int KurExSet
proof
set A = KurExSet;
3 in Int Cl A by Th28,BORSUK_5:14;
hence Int Cl A <> Int Cl Int A by Th27,BORSUK_5:14;
end;
theorem
Int Cl KurExSet <> Cl Int KurExSet
proof
set A = KurExSet;
assume Int Cl A = Cl Int A;
then Int Cl A = {} or Int Cl A = REAL by BORSUK_5:57;
hence thesis by Th28,BORSUK_5:71;
end;
theorem Th38:
Int Cl KurExSet <> Int KurExSet
proof
set A = KurExSet;
A1: 4 in Int Cl A by Th28,BORSUK_5:14;
Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence thesis by A1,BORSUK_5:87;
end;
theorem
Int Cl Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
2 in [. 2,+infty.[ by BORSUK_5:15;
then 2 in Cl A by Th12,XBOOLE_0:def 2;
hence thesis by Th27,BORSUK_5:14;
end;
theorem Th40:
Cl Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
2 in [. 2,+infty.[ by BORSUK_5:15;
then 2 in Cl A by Th12,XBOOLE_0:def 2;
hence thesis by Th26,BORSUK_5:15;
end;
theorem
Int KurExSet <> Cl KurExSet
proof
set A = KurExSet;
4 in [. 2,+infty.[ by BORSUK_5:15;
then A1: 4 in Cl A by Th12,XBOOLE_0:def 2;
Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence thesis by A1,BORSUK_5:87;
end;
theorem Th42:
Cl KurExSet <> KurExSet
proof
set A = KurExSet;
4 in [. 2,+infty.[ by BORSUK_5:15;
then A1: 4 in Cl A by Th12,XBOOLE_0:def 2;
A2: not 4 in ]. 3, 4 .[ by JORDAN6:45;
A3: not 4 in ]. 4,+infty.[ by BORSUK_5:14;
not 4 in {1} & not 4 in RAT (2, 3) by BORSUK_5:52,TARSKI:def 1;
then not 4 in {1} \/ RAT (2, 3) by XBOOLE_0:def 2;
then not 4 in {1} \/ RAT (2, 3) \/ ]. 3, 4 .[ by A2,XBOOLE_0:def 2;
hence thesis by A1,A3,Def6,XBOOLE_0:def 2;
end;
theorem Th43:
KurExSet <> Int KurExSet
proof
set A = KurExSet;
1 in { 1 } by TARSKI:def 1;
then 1 in {1} \/ RAT (2,3) by XBOOLE_0:def 2;
then 1 in {1} \/ RAT (2,3) \/ ]. 3, 4 .[ by XBOOLE_0:def 2;
then A1: 1 in A by Def6,XBOOLE_0:def 2;
Int A = ]. 3, 4 .[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence thesis by A1,BORSUK_5:86;
end;
theorem
Cl Int KurExSet <> Int Cl Int KurExSet
proof
set A = KurExSet;
3 in Cl Int A by Th26,BORSUK_5:15;
hence Cl Int A <> Int Cl Int A by Th27,BORSUK_5:14;
end;
theorem Th45:
Int Cl Int KurExSet <> Int KurExSet
proof
set A = KurExSet;
A1: 4 in Int Cl Int A by Th27,BORSUK_5:14;
Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence Int Cl Int A <> Int A by A1,BORSUK_5:87;
end;
theorem
Cl Int KurExSet <> Int KurExSet
proof
set A = KurExSet;
A1: 3 in Cl Int A by Th26,BORSUK_5:15;
Int A = ]. 3, 4.[ \/ ]. 4,+infty.[ by Th20,TOPS_1:def 1;
hence Cl Int A <> Int A by A1,BORSUK_5:86;
end;
begin :: Final Proofs For Seven
theorem Th47:
Int Cl Int KurExSet <> Int Cl KurExSet
proof
set A = KurExSet;
not 3 in Int Cl Int A by Th27,BORSUK_5:14;
hence thesis by Th28,BORSUK_5:14;
end;
theorem Th48:
Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet are_mutually_different
proof
set A1 = Int KurExSet, A2 = Int Cl KurExSet, A3 = Int Cl Int KurExSet;
thus A1 <> A2 by Th38;
thus A2 <> A3 by Th47;
thus A3 <> A1 by Th45;
end;
theorem Th49:
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_different
proof
set A1 = Cl KurExSet, A2 = Cl Int KurExSet, A3 = Cl Int Cl KurExSet;
thus A1 <> A2 by Th40;
thus A2 <> A3 by Th33;
thus A3 <> A1 by Th31;
end;
theorem Th50:
for X being set st X in
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } holds
X is open non empty Subset of R^1
proof
let X be set;
assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
per cases by A1,ENUMSET1:13;
suppose X = Int KurExSet;
hence thesis by Th20,TOPS_1:def 1;
suppose X = Int Cl KurExSet;
hence thesis by Th28;
suppose X = Int Cl Int KurExSet;
hence thesis by Th27;
end;
theorem
for X being set st X in
{ Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } holds
X is closed Subset of R^1 by ENUMSET1:13;
theorem Th52:
for X being set st X in
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } holds
X <> REAL
proof
let X be set;
assume
A1: X in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet };
per cases by A1,ENUMSET1:13;
suppose X = Int KurExSet;
hence thesis by Th25,BORSUK_5:87;
suppose X = Int Cl KurExSet;
hence thesis by Th28,BORSUK_5:71;
suppose X = Int Cl Int KurExSet;
hence thesis by Th27,BORSUK_5:71;
end;
theorem
for X being set st X in
{ Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } holds
X <> REAL
proof
let X be set;
assume
A1: X in { Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
per cases by A1,ENUMSET1:13;
suppose
A2: X = Cl KurExSet;
A3: not 0 in {1} by TARSKI:def 1;
not 0 in [. 2,+infty.[ by BORSUK_5:15;
hence thesis by A2,A3,Th12,XBOOLE_0:def 2;
suppose X = Cl Int KurExSet;
hence thesis by Th26,BORSUK_5:72;
suppose X = Cl Int Cl KurExSet;
hence thesis by Th29,BORSUK_5:72;
end;
theorem Th54:
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet } misses
{ Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet }
proof
set X = { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet },
Y = { Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet };
assume X meets Y;
then consider x being set such that
A1: x in X & x in Y by XBOOLE_0:3;
x is open non empty Subset of R^1 &
x is closed Subset of R^1 by A1,Th50,ENUMSET1:13;
then x = REAL by BORSUK_5:57;
hence thesis by A1,Th52;
end;
theorem Th55:
Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet
are_mutually_different by Th48,Th49,Th54,BORSUK_5:7;
definition
cluster KurExSet -> non closed non open;
coherence by Th42,Th43,PRE_TOPC:52,TOPS_1:55;
end;
theorem Th56:
{ Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } misses { KurExSet }
proof
set A = KurExSet;
assume { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } meets { KurExSet };
then A1: KurExSet in { Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet } by ZFMISC_1:56;
per cases by A1,ENUMSET1:28;
suppose A = Int A;
hence thesis;
suppose A = Int Cl A;
hence thesis;
suppose A = Int Cl Int A;
hence thesis;
suppose A = Cl A;
hence thesis;
suppose A = Cl Int A;
hence thesis;
suppose A = Cl Int Cl A;
hence thesis;
end;
theorem Th57:
KurExSet, Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet are_mutually_different
proof
Int KurExSet, Int Cl KurExSet, Int Cl Int KurExSet,
Cl KurExSet, Cl Int KurExSet, Cl Int Cl KurExSet, KurExSet
are_mutually_different by Th55,Th56,BORSUK_5:8;
hence thesis by BORSUK_5:9;
end;
theorem
card Kurat7Set KurExSet = 7
proof
set A = KurExSet;
A1: Kurat7Set A = { A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A,
Int Cl Int A } by Def5;
A, Int A, Cl A, Int Cl A, Cl Int A, Cl Int Cl A, Int Cl Int A
are_mutually_different by Th57,BORSUK_5:10;
hence thesis by A1,BORSUK_5:5;
end;
begin :: Final Proofs For Fourteen
definition
cluster Kurat14ClPart KurExSet -> with_proper_subsets;
coherence
proof
set A = KurExSet;
assume the carrier of R^1 in Kurat14ClPart KurExSet;
then A1: REAL in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3,TOPMETR:24;
per cases by A1,ENUMSET1:28;
suppose REAL = Cl A;
hence thesis by Th12,BORSUK_5:103;
suppose REAL = Cl (Cl A)`;
hence thesis by Th14,BORSUK_5:73;
suppose REAL = Cl (Cl (Cl A)`)`;
hence thesis by Th16,BORSUK_5:72;
suppose REAL = Cl A`;
hence thesis by Th19,BORSUK_5:104;
suppose REAL = Cl (Cl A`)`;
hence thesis by Th21,BORSUK_5:72;
suppose REAL = Cl (Cl (Cl A`)`)`;
hence thesis by Th23,BORSUK_5:73;
end;
cluster Kurat14OpPart KurExSet -> with_proper_subsets;
coherence
proof
set A = KurExSet;
assume the carrier of R^1 in Kurat14OpPart KurExSet;
then A2: REAL in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4,TOPMETR:24;
per cases by A2,ENUMSET1:28;
suppose REAL = (Cl A)`;
hence thesis by Th12,BORSUK_5:106;
suppose REAL = (Cl (Cl A)`)`;
hence thesis by Th14,BORSUK_5:106;
suppose REAL = (Cl (Cl (Cl A)`)`)`;
hence thesis by Th16,BORSUK_5:106;
suppose REAL = (Cl A`)`;
hence thesis by Th19,BORSUK_5:106;
suppose REAL = (Cl (Cl A`)`)`;
hence thesis by Th21,BORSUK_5:106;
suppose REAL = (Cl (Cl (Cl A`)`)`)`;
hence thesis by Th23,BORSUK_5:106;
end;
end;
definition
cluster Kurat14Set KurExSet -> with_proper_subsets;
coherence
proof
{ KurExSet, KurExSet` } is Subset-Family of R^1
by MEASURE1:7;
then reconsider AA = { KurExSet, KurExSet` } as Subset-Family of R^1
;
AA is with_proper_subsets
proof
assume
A1: the carrier of R^1 in AA;
per cases by A1,TARSKI:def 2,TOPMETR:24;
suppose REAL = KurExSet;
then [#]R^1 = KurExSet by PRE_TOPC:12,TOPMETR:24;
hence thesis;
suppose REAL = KurExSet`;
then [#]R^1 = KurExSet` by PRE_TOPC:12,TOPMETR:24;
hence thesis by TOPS_1:29;
end;
then A2: AA \/ Kurat14ClPart KurExSet is with_proper_subsets by BORSUK_5:115;
Kurat14Set KurExSet =
AA \/ Kurat14ClPart KurExSet \/ Kurat14OpPart KurExSet by Th5;
hence thesis by A2,BORSUK_5:115;
end;
end;
definition
cluster Kurat14Set KurExSet -> with_non-empty_elements;
coherence
proof
reconsider E = {}R^1 as Subset of R^1;
assume {} in Kurat14Set KurExSet;
then E` in Kurat14Set KurExSet by Th6;
then [#]R^1 in Kurat14Set KurExSet by PRE_TOPC:27;
then the carrier of R^1 in Kurat14Set KurExSet by PRE_TOPC:12;
hence thesis by BORSUK_5:def 6;
end;
end;
theorem Th59:
for A being with_non-empty_elements set,
B being set st B c= A holds
B is with_non-empty_elements
proof
let A be with_non-empty_elements set,
B be set;
assume
A1: B c= A;
assume {} in B;
hence thesis by A1,AMI_1:def 1;
end;
definition
cluster Kurat14ClPart KurExSet -> with_non-empty_elements;
coherence
proof
Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet \/
Kurat14OpPart KurExSet by Th5;
then A1: { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet c= Kurat14Set
KurExSet
by XBOOLE_1:7;
Kurat14ClPart KurExSet c= { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet
by XBOOLE_1:7;
then Kurat14ClPart KurExSet c= Kurat14Set KurExSet by A1,XBOOLE_1:1;
hence thesis by Th59;
end;
cluster Kurat14OpPart KurExSet -> with_non-empty_elements;
coherence
proof
Kurat14Set KurExSet = { KurExSet, KurExSet`} \/ Kurat14ClPart KurExSet \/
Kurat14OpPart KurExSet by Th5;
then Kurat14OpPart KurExSet c= Kurat14Set KurExSet by XBOOLE_1:7;
hence thesis by Th59;
end;
end;
definition
cluster with_proper_subsets with_non-empty_elements Subset-Family of R^1;
existence
proof
take Kurat14Set KurExSet;
thus thesis;
end;
end;
theorem Th60:
for F, G being with_proper_subsets with_non-empty_elements
Subset-Family of R^1 st
F is open & G is closed holds F misses G
proof
let F, G be with_proper_subsets with_non-empty_elements
Subset-Family of R^1;
assume
A1: F is open & G is closed;
assume F meets G;
then consider x being set such that
A2: x in F and
A3: x in G by XBOOLE_0:3;
reconsider x as Subset of R^1 by A2;
A4: x is open by A1,A2,BORSUK_5:def 7;
x is closed by A1,A3,BORSUK_5:def 8;
then x = {} or x = REAL by A4,BORSUK_5:57;
hence thesis by A2,AMI_1:def 1,BORSUK_5:def 6,TOPMETR:24;
end;
definition
cluster Kurat14ClPart KurExSet -> closed;
coherence
proof
set A = KurExSet;
let P be Subset of R^1;
assume P in Kurat14ClPart KurExSet;
then P in { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
hence thesis by ENUMSET1:28;
end;
cluster Kurat14OpPart KurExSet -> open;
coherence
proof
set A = KurExSet;
let P be Subset of R^1;
assume P in Kurat14OpPart KurExSet;
then P in { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
hence thesis by ENUMSET1:28;
end;
end;
theorem Th61:
Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th60;
definition let T, A;
cluster Kurat14ClPart A -> finite;
coherence
proof
Kurat14ClPart A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
hence thesis;
end;
cluster Kurat14OpPart A -> finite;
coherence
proof
Kurat14OpPart A = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
hence thesis;
end;
end;
theorem Th62:
card (Kurat14ClPart KurExSet) = 6
proof
set A = KurExSet;
A1: Kurat14ClPart A = { Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`,
Cl A`, Cl (Cl A`)`, Cl (Cl (Cl A`)`)` } by Def3;
A2: Cl (Cl (Cl A`)`)` = ].-infty, 3 .] by Th22,BORSUK_5:77;
A3: not 3 in Cl (Cl A)` by Th14,BORSUK_5:16;
not 5 in ].-infty, 3 .] & not 5 in {4} by BORSUK_5:16,TARSKI:def 1;
then A4: not 5 in Cl A` by Th19,XBOOLE_0:def 2;
A5: not 4 in Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
4 in [. 2,+infty.[ by BORSUK_5:15;
then A6: Cl A <> Cl (Cl (Cl A`)`)` by A5,Th12,XBOOLE_0:def 2;
A7: Cl (Cl (Cl A)`)` = [. 2,+infty.[ by Th15,BORSUK_5:75;
A8: 3 in Cl (Cl (Cl A)`)` by Th16,BORSUK_5:15;
A9: Cl (Cl A)` <> Cl (Cl (Cl A`)`)` by A2,A3,BORSUK_5:16;
A10: Cl (Cl (Cl A)`)` <> Cl A` by A4,A7,BORSUK_5:15;
4 in Cl (Cl (Cl A)`)` by Th16,BORSUK_5:15;
then A11: Cl (Cl (Cl A)`)` <> Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
A12: Cl Int Cl A = Cl (Cl (Cl A)`)` & Cl Int A = Cl (Cl A`)` by TOPS_1:def 1;
4 in {4} by TARSKI:def 1;
then A13: 4 in Cl A` by Th19,XBOOLE_0:def 2;
A14: not 4 in Cl (Cl (Cl A`)`)` by Th23,BORSUK_5:16;
A15: Cl A` <> Cl (Cl (Cl A`)`)` by A2,A13,BORSUK_5:16;
Cl (Cl A`)` = [. 3,+infty.[ by Th20,BORSUK_5:81;
then Cl (Cl A`)` <> Cl (Cl (Cl A`)`)` by A14,BORSUK_5:15;
then Cl A, Cl (Cl A)`, Cl (Cl (Cl A)`)`, Cl A`,
Cl (Cl A`)`, Cl (Cl (Cl A`)`)`
are_mutually_different by A3,A6,A8,A9,A10,A11,A12,A15,Th31,Th33,BORSUK_5
:def 1;
hence thesis by A1,BORSUK_5:4;
end;
theorem Th63:
card (Kurat14OpPart KurExSet) = 6
proof
set A = KurExSet;
A1: Kurat14OpPart A = { (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`, (Cl (Cl (Cl A`)`)`)` } by Def4;
A2: (Cl A)` = ].-infty, 1 .[ \/ ]. 1, 2 .[ by Th12,BORSUK_5:95;
A3: (Cl (Cl (Cl A)`)`)` = ].-infty, 2 .[ by Th16,BORSUK_5:99;
A4: (Cl (Cl (Cl A`)`)`)` = ]. 3,+infty.[ by Th23,BORSUK_5:98;
A5: 3 in (Cl (Cl A)`)` by Th15,BORSUK_5:14;
5 in ]. 4,+infty.[ by BORSUK_5:14;
then A6: 5 in (Cl A`)` by Th20,XBOOLE_0:def 2;
A7: 4 in (Cl (Cl (Cl A`)`)`)` by Th24,BORSUK_5:14;
not 4 in ].-infty, 1 .[ & not 4 in ]. 1, 2 .[
by BORSUK_5:17,JORDAN6:45;
then A8: (Cl A)` <> (Cl (Cl (Cl A`)`)`)` by A2,A7,XBOOLE_0:def 2;
(Cl A)` <> (Cl Int Cl A)` by Th31,BORSUK_5:105;
then A9: (Cl A)` <> (Cl (Cl (Cl A)`)`)` by TOPS_1:def 1;
A10: (Cl (Cl A)`)` <> (Cl (Cl (Cl A)`)`)` by A3,A5,BORSUK_5:17;
A11: (Cl (Cl A)`)` <> (Cl (Cl (Cl A`)`)`)` by A4,A5,BORSUK_5:14;
A12: (Cl (Cl (Cl A)`)`)` <> (Cl A`)` by A3,A6,BORSUK_5:17;
A13: not 4 in (Cl (Cl (Cl A)`)`)` by Th17,BORSUK_5:17;
(Cl Int Cl A)` = (Cl (Cl (Cl A)`)`)` & (Cl Int A)` = (Cl (Cl A`)`)`
by TOPS_1:def 1;
then A14: (Cl (Cl (Cl A)`)`)` <> (Cl (Cl A`)`)` by Th33,BORSUK_5:105;
A15: not 4 in ]. 3, 4 .[ by JORDAN6:45;
not 4 in ]. 4,+infty.[ by BORSUK_5:14;
then A16: not 4 in (Cl A`)` by A15,Th20,XBOOLE_0:def 2;
A17: 4 in (Cl (Cl (Cl A`)`)`)` by Th24,BORSUK_5:14;
not 4 in (Cl (Cl A`)`)` by Th22,BORSUK_5:17;
then (Cl A)`, (Cl (Cl A)`)`, (Cl (Cl (Cl A)`)`)`,
(Cl A`)`, (Cl (Cl A`)`)`,
(Cl (Cl (Cl A`)`)`)` are_mutually_different
by A8,A9,A10,A11,A12,A13,A14,A16,A17,BORSUK_5:def 1;
hence thesis by A1,BORSUK_5:4;
end;
theorem Th64:
{ KurExSet, KurExSet` } misses Kurat14ClPart KurExSet
proof
set A = KurExSet;
assume { A, A` } meets Kurat14ClPart A;
then consider x being set such that
A1: x in { A, A` } & x in Kurat14ClPart A by XBOOLE_0:3;
reconsider x as Subset of R^1 by A1;
A2: x is closed by A1,BORSUK_5:def 8;
x = A or x = A` by A1,TARSKI:def 2;
then x` = A by A1,BORSUK_5:def 8;
hence thesis by A2,TOPS_1:29;
end;
definition
cluster KurExSet -> non empty;
coherence by Def6;
end;
theorem Th65:
KurExSet <> KurExSet`
proof
assume KurExSet = KurExSet`;
then KurExSet meets KurExSet` by XBOOLE_1:66;
hence thesis by PRE_TOPC:26;
end;
theorem Th66:
{ KurExSet, KurExSet` } misses Kurat14OpPart KurExSet
proof
set A = KurExSet;
assume { A, A` } meets Kurat14OpPart A;
then consider x being set such that
A1: x in { A, A` } & x in Kurat14OpPart A by XBOOLE_0:3;
reconsider x as Subset of R^1 by A1;
A2: x is open by A1,BORSUK_5:def 7;
x = A or x = A` by A1,TARSKI:def 2;
then x` = A by A1,BORSUK_5:def 7;
hence thesis by A2,TOPS_1:30;
end;
theorem
card Kurat14Set KurExSet = 14
proof
set A = KurExSet;
A1: card (Kurat14ClPart A \/ Kurat14OpPart A) = 6 + 6
by Th61,Th62,Th63,CARD_2:53
.= 12;
set B = { A, A` };
A2: B misses (Kurat14ClPart A \/ Kurat14OpPart A) by Th64,Th66,XBOOLE_1:70;
card Kurat14Set A = card (B \/ Kurat14ClPart A \/ Kurat14OpPart A) by Th5
.= card (B \/ (Kurat14ClPart A \/ Kurat14OpPart A)) by XBOOLE_1:4
.= card B + card (Kurat14ClPart A \/ Kurat14OpPart A) by A2,CARD_2:53
.= 2 + 12 by A1,Th65,CARD_2:76
.= 14;
hence thesis;
end;
begin :: Properties of Kuratowski Sets
definition let T be TopStruct, A be Subset-Family of T;
attr A is Cl-closed means
for P being Subset of T st
P in A holds Cl P in A;
attr A is Int-closed means
for P being Subset of T st
P in A holds Int P in A;
end;
definition let T be 1-sorted, A be Subset-Family of T;
attr A is compl-closed means
for P being Subset of T st
P in A holds P` in A;
end;
definition let T, A;
cluster Kurat14Set A -> non empty;
coherence by Th3;
cluster Kurat14Set A -> Cl-closed;
coherence
proof
let P be Subset of T;
assume P in Kurat14Set A;
hence thesis by Th6;
end;
cluster Kurat14Set A -> compl-closed;
coherence
proof
let P be Subset of T;
assume P in Kurat14Set A;
hence thesis by Th6;
end;
end;
definition let T, A;
cluster Kurat7Set A -> non empty;
coherence by Th8;
cluster Kurat7Set A -> Int-closed;
coherence
proof
let P be Subset of T;
assume P in Kurat7Set A;
hence thesis by Th10;
end;
cluster Kurat7Set A -> Cl-closed;
coherence
proof
let P be Subset of T;
assume P in Kurat7Set A;
hence thesis by Th10;
end;
end;
definition let T;
cluster Int-closed Cl-closed non empty Subset-Family of T;
existence
proof
consider A being Subset of T;
take Kurat7Set A;
thus thesis;
end;
cluster compl-closed Cl-closed non empty Subset-Family of T;
existence
proof
consider A being Subset of T;
take Kurat14Set A;
thus thesis;
end;
end;