A1: {(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 A1, Lm1; :: thesis: verum