theorem Th17: :: WAYBEL_6:17

for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )