:: deftheorem Def19 defines lower WAYBEL_0:def 19 :
for L being RelStr
for X being Subset of L holds
( X is lower iff for x, y being Element of L st x in X & y <= x holds
y in X );