T in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of : t is Tolerance of } ;
then consider t being Element of Toler_on_subsets X, Y being Subset of such that
A1: T = [t,Y] and
A2: t is Tolerance of ;
T `2 = Y by A1, MCART_1:def 2;
hence T `1 is Tolerance of by A1, A2, MCART_1:def 1; :: thesis: verum