theorem Th8: :: YELLOW21:8

for P being non empty reflexive RelStr holds
( P is upper-bounded iff the InternalRel of P is upper-bounded )