theorem :: WAYBEL_6:16

for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )