:: deftheorem defines order-generating WAYBEL_6:def 5 :
for L being non empty RelStr
for X being Subset of L holds
( X is order-generating iff for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );