theorem Th9: :: NECKLA_3:9

for G being irreflexive RelStr
for G1, G2 being RelStr st ( G = union_of (G1,G2) or G = sum_of (G1,G2) ) holds
( G1 is irreflexive & G2 is irreflexive )