for L being upper-bounded LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff (downarrow l) ` is Filter of L )