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;