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 p9, q9 be Element of (L .: ); :: thesis: ( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I )
p9 "/\" q9 = (.: p9) "\/" (.: q9) ;
hence ( ( p9 in I & q9 in I ) iff p9 "/\" q9 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