theorem :: ZFMISC_1:89

for X1, X2, Y1, Y2 being set st ( for x, y being object holds
( [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:] ) ) holds
[:X1,Y1:] = [:X2,Y2:]