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 Th19;
hence ( x is prime Filter of L iff x is prime Ideal of (L opp ) ) by Th20; :: thesis: verum