theorem :: COH_SP:32

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