theorem Th20: :: FILTER_2:20

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