:: deftheorem defines Toler_on_subsets COH_SP:def 17 :
for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ;