for X being set holds Total X in Toler_on_subsets X by Th29;