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