for L being lower-bounded continuous LATTICE
for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )