theorem Th84: :: ZFMISC_1:85

for z being object
for X1, X2, Y1, Y2 being set st z in [:X1,Y1:] /\ [:X2,Y2:] holds
ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )