theorem Th35: :: NECKLA_3:35

for G being RelStr
for H1, H2 being non empty RelStr
for x being Element of H1
for y being Element of H2 st G = union_of (H1,H2) & the carrier of H1 misses the carrier of H2 holds
not [x,y] in the InternalRel of G