theorem :: ZFMISC_1:119

for N, M, X1, X2, Y1, Y2 being set st N c= [:X1,Y1:] & M c= [:X2,Y2:] holds
N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]