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