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 (L opp); :: 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 L; :: 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