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