for L being LATTICE
for x being set holds
( x is prime Filter of L iff x is prime Ideal of (L opp) )