A2: {((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} is Subset-Family of T by MEASURE1:3;
( {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} = {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `)} \/ {((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `)} is Subset-Family of T ) by ENUMSET1:13, MEASURE1:3;
hence {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T by A2, Lm1; :: thesis: verum