theorem :: COH_SP:38

for X being set holds [(Total X),X] in TOL X by Th35;