theorem Th1: :: ROUGHS_1:1

for X being set st Total X c= id X holds
X is trivial