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