let T be non empty TopSpace; for A, Q being Subset of T st Q in Kurat14Set A holds
( Q ` in Kurat14Set A & Q - in Kurat14Set A )
let A, Q be Subset of T; ( Q in Kurat14Set A implies ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) )
set k1 = Cl A;
set k2 = (Cl A) ` ;
set k3 = Cl ((Cl A) `);
set k4 = (Cl ((Cl A) `)) ` ;
set k5 = Cl ((Cl ((Cl A) `)) `);
set k6 = (Cl ((Cl ((Cl A) `)) `)) ` ;
set k7 = Cl (A `);
set k8 = (Cl (A `)) ` ;
set k9 = Cl ((Cl (A `)) `);
set k10 = (Cl ((Cl (A `)) `)) ` ;
set k11 = Cl ((Cl ((Cl (A `)) `)) `);
set k12 = (Cl ((Cl ((Cl (A `)) `)) `)) ` ;
assume A1:
Q in Kurat14Set A
; ( Q ` in Kurat14Set A & Q - in Kurat14Set A )
per cases
( Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} or Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by A1, XBOOLE_0:def 3;
suppose A2:
Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}
;
( Q ` in Kurat14Set A & Q - in Kurat14Set A )
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
proof
per cases
( Q = A or Q = Cl A or Q = (Cl A) ` or Q = Cl ((Cl A) `) or Q = (Cl ((Cl A) `)) ` or Q = Cl ((Cl ((Cl A) `)) `) or Q = (Cl ((Cl ((Cl A) `)) `)) ` )
by A2, ENUMSET1:def 5;
suppose
Q = A
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl A
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = (Cl A) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl ((Cl A) `)
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = (Cl ((Cl A) `)) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl ((Cl ((Cl A) `)) `)
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose A3:
Q = (Cl ((Cl ((Cl A) `)) `)) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )
Cl ((Cl ((Cl ((Cl A) `)) `)) `) = Cl ((Cl A) `)
by Th1;
then A4:
Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}
by A3, ENUMSET1:def 5;
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}
by A3, ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by A4, XBOOLE_0:def 3;
verum end; end;
end; hence
(
Q ` in Kurat14Set A &
Q - in Kurat14Set A )
;
verum end; suppose A5:
Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}
;
( Q ` in Kurat14Set A & Q - in Kurat14Set A )
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
proof
per cases
( Q = A ` or Q = Cl (A `) or Q = (Cl (A `)) ` or Q = Cl ((Cl (A `)) `) or Q = (Cl ((Cl (A `)) `)) ` or Q = Cl ((Cl ((Cl (A `)) `)) `) or Q = (Cl ((Cl ((Cl (A `)) `)) `)) ` )
by A5, ENUMSET1:def 5;
suppose
Q = A `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl (A `)
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = (Cl (A `)) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl ((Cl (A `)) `)
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = (Cl ((Cl (A `)) `)) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose
Q = Cl ((Cl ((Cl (A `)) `)) `)
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
(
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} &
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} )
by ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by XBOOLE_0:def 3;
verum end; suppose A6:
Q = (Cl ((Cl ((Cl (A `)) `)) `)) `
;
( Q ` in Kurat14Set A & Cl Q in Kurat14Set A )then
Cl Q = Cl ((Cl (A `)) `)
by Th1;
then A7:
Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}
by ENUMSET1:def 5;
Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}
by A6, ENUMSET1:def 5;
hence
(
Q ` in Kurat14Set A &
Cl Q in Kurat14Set A )
by A7, XBOOLE_0:def 3;
verum end; end;
end; hence
(
Q ` in Kurat14Set A &
Q - in Kurat14Set A )
;
verum end; end;