theorem Th37: :: NECKLA_3:37

for G being non empty symmetric RelStr
for x being Element of G
for R1, R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 & subrelstr (([#] G) \ {x}) = union_of (R1,R2) & G is path-connected holds
ex b being Element of R1 st [b,x] in the InternalRel of G