let T be non empty TopSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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) ` )) ` )) ` )} ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl A ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = (Cl A) ` ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl ((Cl A) ` ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = (Cl ((Cl A) ` )) ` ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl ((Cl ((Cl A) ` )) ` ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose A3: Q = (Cl ((Cl ((Cl A) ` )) ` )) ` ; :: thesis: ( 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; :: thesis: verum

end;

end;

end;

hence ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ; :: thesis: 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 ` )) ` )) ` )) ` )} ; :: thesis: ( 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 ` ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl (A ` ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = (Cl (A ` )) ` ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl ((Cl (A ` )) ` ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = (Cl ((Cl (A ` )) ` )) ` ; :: thesis: ( 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; :: thesis: verum

end;

suppose Q = Cl ((Cl ((Cl (A ` )) ` )) ` ) ; :: thesis: ( 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; :: thesis: verum

end;

suppose A6: Q = (Cl ((Cl ((Cl (A ` )) ` )) ` )) ` ; :: thesis: ( 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; :: thesis: verum

end;

end;

end;

hence ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ; :: thesis: verum

end;

end;