:: deftheorem Def1 defines lower WELLFND1:def 1 :
for R being RelStr
for X being Subset of R holds
( X is lower iff for x, y being object st x in X & [y,x] in the InternalRel of R holds
y in X );