let L be Lattice; :: thesis: for x being set holds
( x is Ideal of L iff x is Filter of L .: )
let x be set ; :: thesis: ( x is Ideal of L iff x is Filter of L .: )
thus ( x is Ideal of L implies x is Filter of L .: ) :: thesis: ( x is Filter of L .: implies x is Ideal of L )

proof

assume x is Ideal of L ; :: thesis: x is Filter of L .:
then reconsider I = x as Ideal of L ;
reconsider I = I as non empty Subset of ;
I is Filter of L .:

proof

now

let p', q' be Element of ; :: thesis: ( ( p' in I & q' in I ) iff p' "/\" q' in I )
p' "/\" q' = (.: p') "\/" (.: q') ;
hence ( ( p' in I & q' in I ) iff p' "/\" q' in I ) by Def3; :: thesis: verum

end;

hence I is Filter of L .: by FILTER_0:8; :: thesis: verum

end;

hence x is Filter of L .: ; :: thesis: verum

end;

assume x is Filter of L .: ; :: thesis: x is Ideal of L
then reconsider F = x as Filter of L .: ;
reconsider F = F as non empty Subset of ;

now

let p, q be Element of ; :: thesis: ( ( p in F & q in F ) iff p "\/" q in F )
(p .: ) "/\" (q .: ) = p "\/" q ;
hence ( ( p in F & q in F ) iff p "\/" q in F ) by FILTER_0:8; :: thesis: verum

end;

hence x is Ideal of L by Def3; :: thesis: verum