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

let p' be Element of (L .: ); :: according to FILTER_0:def 1 :: thesis: for b₁ being Element of the carrier of (L .: ) holds
( ( not p' in I or not b₁ in I or p' "/\" b₁ in I ) & ( not p' "/\" b₁ in I or ( p' in I & b₁ in I ) ) )
let q' be Element of (L .: ); :: thesis: ( ( not p' in I or not q' in I or p' "/\" q' in I ) & ( not p' "/\" q' in I or ( p' in I & q' in I ) ) )
( p' = .: p' & q' = .: q' & p' "/\" q' = (.: p') "\/" (.: q') ) ;
hence ( ( not p' in I or not q' in I or p' "/\" q' in I ) & ( not p' "/\" q' in I or ( p' in I & q' in I ) ) ) by Def3; :: 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 = p .: & q = q .: & (p .: ) "/\" (q .: ) = p "\/" q ) ;
hence ( ( p in F & q in F ) iff p "\/" q in F ) by FILTER_0:def 1; :: thesis: verum

end;

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