let L be Lattice; :: thesis: for S being non empty Subset of L holds
( S is Filter of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) )
let S be non empty Subset of L; :: thesis: ( S is Filter of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) )
thus ( S is Filter of L implies for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ) :: thesis: ( ( for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ) implies S is Filter of L )

proof

assume ZZ: S is Filter of L ; :: thesis: for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S )
let p, q be Element of L; :: thesis: ( ( p in S & q in S ) iff p "/\" q in S )
thus ( p in S & q in S implies p "/\" q in S ) by ZZ, LATTICES:def 24; :: thesis: ( p "/\" q in S implies ( p in S & q in S ) )
assume Z: p "/\" q in S ; :: thesis: ( p in S & q in S )
( p "/\" q [= p & p "/\" q [= q ) by LATTICES:23;
hence ( p in S & q in S ) by ZZ, Z, LATTICES:def 23; :: thesis: verum

end;

assume Z: for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ; :: thesis: S is Filter of L
then A: S is meet-closed by LATTICES:def 24;
S is final

proof

let p, q be Element of L; :: according to LATTICES:def 23 :: thesis: ( not p [= q or not p in S or q in S )
assume that
Z1: p [= q and
Z2: p in S ; :: thesis: q in S
p "/\" q = p by Z1, LATTICES:21;
hence q in S by Z, Z2; :: thesis: verum

end;

hence S is Filter of L by A; :: thesis: verum