theorem Th99: :: ZFMISC_1:100

for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]