for X being set
for Y being lower Subset of (BoolePoset X) holds
( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )