for L being distributive continuous LATTICE
for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
p is pseudoprime