theorem :: ZFMISC_1:87

for X, Y being set
for x, y being object holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) ) by Lm16;