theorem :: ZFMISC_1:113

for e being object
for X1, X2, Y1, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]