:: deftheorem defines directed QUANTAL1:def 1 :
for L being non empty LattStr
for X being Subset of L holds
( X is directed iff for Y being finite Subset of X ex x being Element of L st
( "\/" (Y,L) [= x & x in X ) );