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