let X1, X2, Y1, Y2 be set ; :: thesis: [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]
thus [:(X1 \/ X2),(Y1 \/ Y2):] = [:X1,(Y1 \/ Y2):] \/ [:X2,(Y1 \/ Y2):] by Th96
.= ([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,(Y1 \/ Y2):] by Th96
.= ([:X1,Y1:] \/ [:X1,Y2:]) \/ ([:X2,Y1:] \/ [:X2,Y2:]) by Th96
.= (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:] by XBOOLE_1:4 ; :: thesis: verum