theorem Th15: :: WAYBEL_6:15

for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )