theorem Th35: :: COH_SP:36

for a, X being set st a c= X holds
[(Total a),a] in TOL X