theorem Th3: :: SETLIM_2:3

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