theorem Th42: :: WAYBEL_0:42

for L being with_suprema Poset
for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )