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