for L being Lattice
for F being Filter of L
for p, q being Element of L st p in <.(<.q.) \/ F).) holds
ex r being Element of L st
( r in F & q "/\" r [= p )