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