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 :: thesis: for p9, q9 being Element of (L .:) holds
( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I )

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 Lm1; :: 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 :: thesis: for p, q being Element of L holds
( ( p in F & q in F ) iff p "\/" q in F )

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 Lm1; :: thesis: verum