theorem :: WAYBEL_7:10

for X being set
for Y being non empty lower Subset of (BoolePoset X) holds
( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )