:: deftheorem defines [ TARSKI:def 5 :
for x, y being object holds [x,y] = {{x,y},{x}};