for L being lower-bounded distributive continuous LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )