let L be LATTICE; :: thesis: for x being set holds
( x is prime Filter of L iff x is prime Ideal of (L opp) )
let x be set ; :: thesis: ( x is prime Filter of L iff x is prime Ideal of (L opp) )
(L opp) opp = RelStr(# the carrier of L, the InternalRel of L #) by LATTICE3:8;
then ( x is prime Filter of L iff x is prime Filter of ((L opp) opp) ) by Th15;
hence ( x is prime Filter of L iff x is prime Ideal of (L opp) ) by Th16; :: thesis: verum