theorem Th27: :: CLASSES1:27
for X, x, y being set st x in Tarski-Class X & y in Tarski-Class X holds
[x,y] in Tarski-Class X