theorem :: COH_SP:28

for a being set holds Total a in Toler a by Def15;