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: Kurat14Part (A ` ) c= Kurat14Set A by XBOOLE_1:7;
( A ` in Kurat14Part (A ` ) & Cl (A ` ) in Kurat14Part (A ` ) & (Cl (A ` )) ` in Kurat14Part (A ` ) & Cl ((Cl (A ` )) ` ) in Kurat14Part (A ` ) & (Cl ((Cl (A ` )) ` )) ` in Kurat14Part (A ` ) & Cl ((Cl ((Cl (A ` )) ` )) ` ) in Kurat14Part (A ` ) & (Cl ((Cl ((Cl (A ` )) ` )) ` )) ` in Kurat14Part (A ` ) ) by ENUMSET1:def 5;
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; :: thesis: verum