theorem Th2: :: TOLER_1:2

for X, x, y being set st x in X & y in X holds
[x,y] in Total X