:: deftheorem Def5 defines upper-bounded YELLOW_0:def 5 :
for L being RelStr holds
( L is upper-bounded iff ex x being Element of L st x is_>=_than the carrier of L );