theorem Th16: :: WAYBEL_7:16

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