theorem Th6: :: LFUZZY_0:6

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 lower-bounded )