theorem :: FUNCT_4:65

for x1, x2, y being object holds (x1,x2) --> (y,y) = {x1,x2} --> y