theorem Th4: :: WELLFND1:4

for R being RelStr
for X being Subset of R
for x being set st X is lower & x in X holds
the InternalRel of R -Seg x c= X