:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def 10 :
for L being non empty \/-SemiLattRelStr holds
( L is naturally_sup-generated iff for x, y being Element of L holds
( x <= y iff x |_| y = y ) );