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