let T be non empty TopSpace; :: thesis: for A being Subset of T holds 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 ` )) ` )) ` )) ` )}
let A be Subset of T; :: thesis: 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 ` )) ` )) ` )) ` )}
set Y1 = {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))};
set Y2 = {A,(A ` )};
set Y3 = {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )};
set Y = ({(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 ` )) ` )) ` )) ` )};
A1: {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} c= ({(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 XBOOLE_1:7;
A2: ({(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 ` )) ` )) ` )) ` )} c= Kurat14Set A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ({(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 ` )) ` )) ` )) ` )} or x in Kurat14Set A )
assume x in ({(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 ` )) ` )) ` )) ` )} ; :: thesis: x in Kurat14Set A
then A3: ( 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 3;

per cases ( x in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} or x in {A,(A ` )} or x in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} ) by A3, XBOOLE_0:def 3;

suppose x in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} ; :: thesis: x in Kurat14Set 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:def 4;
hence x in Kurat14Set A by Th3, Th4; :: thesis: verum

end;

suppose x in {A,(A ` )} ; :: thesis: x in Kurat14Set A

then ( x = A or x = A ` ) by TARSKI:def 2;
hence x in Kurat14Set A by Th3, Th4; :: thesis: verum

end;

suppose x in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} ; :: thesis: x in Kurat14Set 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:def 4;
hence x in Kurat14Set A by Th3, Th4; :: thesis: verum

end;

end;

end;

A4: {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} \/ {A,(A ` )} c= ({(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 XBOOLE_1:7;
(Cl ((Cl A) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A5: (Cl ((Cl A) ` )) ` in ({(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 A1;
(Cl A) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A6: (Cl A) ` in ({(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 A1;
{A,(A ` )} c= {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} \/ {A,(A ` )} by XBOOLE_1:7;
then A7: {A,(A ` )} c= ({(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 A4, XBOOLE_1:1;
(Cl ((Cl ((Cl (A ` )) ` )) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A8: (Cl ((Cl ((Cl (A ` )) ` )) ` )) ` in ({(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 A1;
(Cl ((Cl (A ` )) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A9: (Cl ((Cl (A ` )) ` )) ` in ({(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 A1;
(Cl (A ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A10: (Cl (A ` )) ` in ({(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 A1;
(Cl ((Cl ((Cl A) ` )) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} by ENUMSET1:def 4;
then A11: (Cl ((Cl ((Cl A) ` )) ` )) ` in ({(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 A1;
A in {A,(A ` )} by TARSKI:def 2;
then A12: A in ({(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 A7;
{(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} c= {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} \/ {A,(A ` )} by XBOOLE_1:7;
then A13: {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} c= ({(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 A4, XBOOLE_1:1;
A ` in {A,(A ` )} by TARSKI:def 2;
then A14: A ` in ({(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 A7;
Cl ((Cl ((Cl (A ` )) ` )) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A15: Cl ((Cl ((Cl (A ` )) ` )) ` ) in ({(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 A13;
Cl ((Cl (A ` )) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A16: Cl ((Cl (A ` )) ` ) in ({(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 A13;
Cl (A ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A17: Cl (A ` ) in ({(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 A13;
Cl ((Cl ((Cl A) ` )) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A18: Cl ((Cl ((Cl A) ` )) ` ) in ({(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 A13;
Cl ((Cl A) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A19: Cl ((Cl A) ` ) in ({(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 A13;
Cl A in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} by ENUMSET1:def 4;
then A20: Cl A in ({(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 A13;
Kurat14Set A c= ({(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

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Kurat14Set A or x in ({(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 ` )) ` )) ` )) ` )} )
assume A21: x in Kurat14Set A ; :: thesis: x in ({(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 ` )) ` )) ` )) ` )}

per cases ( x in {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} or x in {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} ) by A21, XBOOLE_0:def 3;

suppose x in {A,(Cl A),((Cl A) ` ),(Cl ((Cl A) ` )),((Cl ((Cl A) ` )) ` ),(Cl ((Cl ((Cl A) ` )) ` )),((Cl ((Cl ((Cl A) ` )) ` )) ` )} ; :: thesis: x in ({(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 ` )) ` )) ` )) ` )}

hence x in ({(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 A20, A19, A18, A12, A6, A5, A11, ENUMSET1:def 5; :: thesis: verum

end;

suppose x in {(A ` ),(Cl (A ` )),((Cl (A ` )) ` ),(Cl ((Cl (A ` )) ` )),((Cl ((Cl (A ` )) ` )) ` ),(Cl ((Cl ((Cl (A ` )) ` )) ` )),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} ; :: thesis: x in ({(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 ` )) ` )) ` )) ` )}

hence x in ({(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 A17, A16, A15, A14, A10, A9, A8, ENUMSET1:def 5; :: thesis: verum

end;

end;

end;

hence 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 A2, XBOOLE_0:def 10; :: thesis: verum