theorem Th17: :: WAYBEL_7:17

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