theorem Th7: :: LFUZZY_0:7

for R being non empty real RelStr holds
( ex x being Real st
( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x >= y ) ) iff R is upper-bounded )