theorem :: TOLER_1:3

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