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 (L .: ) ;
I is Filter of (L .: )

proof

now

let p', q' be Element of (L .: ); :: 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 L ;

now

let p, q be Element of L; :: 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