theorem Th8: :: NECKLA_3:8

for R1, R2 being RelStr holds
( union_of (R1,R2) = union_of (R2,R1) & sum_of (R1,R2) = sum_of (R2,R1) )