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