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 ` )) ` )) ` )) ` )} & {(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 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 ` )} & {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 A2:
( {(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 ` )) ` )) ` )) ` )} & {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 A1, XBOOLE_1:1;
A3:
( Cl A in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} & Cl ((Cl A) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} & Cl ((Cl ((Cl A) ` )) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} & Cl (A ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} & Cl ((Cl (A ` )) ` ) in {(Cl A),(Cl ((Cl A) ` )),(Cl ((Cl ((Cl A) ` )) ` )),(Cl (A ` )),(Cl ((Cl (A ` )) ` )),(Cl ((Cl ((Cl (A ` )) ` )) ` ))} & 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;
A4:
( A in {A,(A ` )} & A ` in {A,(A ` )} )
by TARSKI:def 2;
( (Cl A) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} & (Cl ((Cl A) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} & (Cl ((Cl ((Cl A) ` )) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} & (Cl (A ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} & (Cl ((Cl (A ` )) ` )) ` in {((Cl A) ` ),((Cl ((Cl A) ` )) ` ),((Cl ((Cl ((Cl A) ` )) ` )) ` ),((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} & (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 A5:
( 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & 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 ` )) ` )) ` )) ` )} & (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 ` )) ` )) ` )) ` )} & (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 ` )) ` )) ` )) ` )} & (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 ` )) ` )) ` )) ` )} & (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 ` )) ` )) ` )) ` )} & (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 ` )) ` )) ` )) ` )} & (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, A2, A3, A4;
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
thus
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 ` )) ` )) ` )) ` )}
:: according to XBOOLE_0:def 10 :: thesis: ({(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 Aproof
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 A6:
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 A6, 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 A5, 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 A5, ENUMSET1:def 5;
:: thesis: verum end;
end;
thus
({(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
:: thesis: verumproof
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 A7:
(
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 A7, XBOOLE_0:def 3;
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 ` )) ` )) ` )) ` )}
; :: thesis: verum