theorem Th9: :: WAYBEL14:9

for R being non empty reflexive antisymmetric complete RelStr
for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )