:: deftheorem defines TOL COH_SP:def 18 :
for X being set holds TOL X = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ;