let L be LATTICE; :: thesis: for x being set holds
( x is prime Ideal of L iff x is prime Filter of L opp )
let x be set ; :: thesis: ( x is prime Ideal of L iff x is prime Filter of L opp )

hereby :: thesis: ( x is prime Filter of L opp implies x is prime Ideal of L )

assume x is prime Ideal of L ; :: thesis: x is prime Filter of L opp
then reconsider I = x as prime Ideal of L ;
reconsider F = I as Filter of L opp by YELLOW_7:26, YELLOW_7:28;
F is prime

proof

let x, y be Element of ; :: according to WAYBEL_7:def 2 :: thesis: ( not x "\/" y in F or x in F or y in F )
A1: x "\/" y = (~ x) "/\" (~ y) by YELLOW_7:22;
( ~ x = x & ~ y = y ) by LATTICE3:def 7;
hence ( not x "\/" y in F or x in F or y in F ) by A1, Def1; :: thesis: verum

end;

hence x is prime Filter of L opp ; :: thesis: verum

end;

assume x is prime Filter of L opp ; :: thesis: x is prime Ideal of L
then reconsider I = x as prime Filter of L opp ;
reconsider F = I as Ideal of L by YELLOW_7:26, YELLOW_7:28;
F is prime

proof

let x, y be Element of ; :: according to WAYBEL_7:def 1 :: thesis: ( not x "/\" y in F or x in F or y in F )
A2: x "/\" y = (x ~ ) "\/" (y ~ ) by YELLOW_7:21;
( x ~ = x & y ~ = y ) by LATTICE3:def 6;
hence ( not x "/\" y in F or x in F or y in F ) by A2, Def2; :: thesis: verum

end;

hence x is prime Ideal of L ; :: thesis: verum