theorem Th3: :: CLASSES2:3

for x, y, W being set st W is Tarski & x in W & y in W holds
[x,y] in W