let T be non empty TopSpace; :: thesis: for A being Subset of T holds
( A in Kurat14Set A & A - in Kurat14Set A & (A - ) ` in Kurat14Set A & ((A - ) ` ) - in Kurat14Set A & (((A - ) ` ) - ) ` in Kurat14Set A & ((((A - ) ` ) - ) ` ) - in Kurat14Set A & (((((A - ) ` ) - ) ` ) - ) ` in Kurat14Set A )
let A be Subset of T; :: thesis: ( A in Kurat14Set A & A - in Kurat14Set A & (A - ) ` in Kurat14Set A & ((A - ) ` ) - in Kurat14Set A & (((A - ) ` ) - ) ` in Kurat14Set A & ((((A - ) ` ) - ) ` ) - in Kurat14Set A & (((((A - ) ` ) - ) ` ) - ) ` in Kurat14Set A )
A1: ( Cl A in Kurat14Part A & (Cl A) ` in Kurat14Part A ) by ENUMSET1:def 5;
A2: ( Cl ((Cl A) ` ) in Kurat14Part A & (Cl ((Cl A) ` )) ` in Kurat14Part A ) by ENUMSET1:def 5;
A3: ( Cl ((Cl ((Cl A) ` )) ` ) in Kurat14Part A & (Cl ((Cl ((Cl A) ` )) ` )) ` in Kurat14Part A ) by ENUMSET1:def 5;
( Kurat14Part A c= Kurat14Set A & A in Kurat14Part A ) by ENUMSET1:def 5, XBOOLE_1:7;
hence ( A in Kurat14Set A & A - in Kurat14Set A & (A - ) ` in Kurat14Set A & ((A - ) ` ) - in Kurat14Set A & (((A - ) ` ) - ) ` in Kurat14Set A & ((((A - ) ` ) - ) ` ) - in Kurat14Set A & (((((A - ) ` ) - ) ` ) - ) ` in Kurat14Set A ) by A1, A2, A3; :: thesis: verum