theorem Th18: :: NECKLA_3:18

for G1, G2 being RelStr st the carrier of G1 misses the carrier of G2 holds
ComplRelStr (sum_of (G1,G2)) = union_of ((ComplRelStr G1),(ComplRelStr G2))