A2: {((Cl (A ` )) ` ),((Cl ((Cl (A ` )) ` )) ` ),((Cl ((Cl ((Cl (A ` )) ` )) ` )) ` )} is Subset-Family of T by MEASURE1:8;
( {((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:53, MEASURE1:8;
hence {((A - ) ` ),((((A - ) ` ) - ) ` ),((((((A - ) ` ) - ) ` ) - ) ` ),(((A ` ) - ) ` ),(((((A ` ) - ) ` ) - ) ` ),(((((((A ` ) - ) ` ) - ) ` ) - ) ` )} is Subset-Family of T by A2, Lm1; :: thesis: verum