theorem Th3: :: WELLFND1:3

for R being RelStr
for x being set holds the InternalRel of R -Seg x c= the carrier of R