:: deftheorem Def4 defines lower-bounded YELLOW_0:def 4 :
for L being RelStr holds
( L is lower-bounded iff ex x being Element of L st x is_<=_than the carrier of L );