let N, M, X1, Y1, X2, Y2 be set ; :: thesis: ( N c= [:X1,Y1:] & M c= [:X2,Y2:] implies N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):] )
( X1 c= X1 \/ X2 & Y2 c= Y1 \/ Y2 & X2 c= X1 \/ X2 & Y1 c= Y1 \/ Y2 ) by XBOOLE_1:7;
then ( [:X1,Y1:] c= [:(X1 \/ X2),(Y1 \/ Y2):] & [:X2,Y2:] c= [:(X1 \/ X2),(Y1 \/ Y2):] ) by Th119;
then A1: [:X1,Y1:] \/ [:X2,Y2:] c= [:(X1 \/ X2),(Y1 \/ Y2):] by XBOOLE_1:8;
assume ( N c= [:X1,Y1:] & M c= [:X2,Y2:] ) ; :: thesis: N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]
then N \/ M c= [:X1,Y1:] \/ [:X2,Y2:] by XBOOLE_1:13;
hence N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):] by A1, XBOOLE_1:1; :: thesis: verum