theorem :: QUANTAL1:3

for L being non empty LattStr
for X being Subset of L st X is directed holds
not X is empty