theorem Th8: :: SETLIM_2:8

for X being set
for A1, A2 being SetSequence of X holds Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)