for L being lower-bounded continuous LATTICE
for x, y being Element of L holds
( x << y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x << d ) )