theorem Th11: :: SETLIM_2:11
for X being set
for A1, A2 being SetSequence of X holds (Union A1) \+\ (Union A2) c= Union (A1 (\+\) A2)