theorem Th8: :: YELLOW21:8
for P being non empty reflexive RelStr holds
( P is upper-bounded iff the InternalRel of P is upper-bounded )