for L being Lattice
for x being set holds
( x is Ideal of L iff x is Filter of (L .:) )