:: deftheorem Def7 defines => FILTER_0:def 7 :
for L being Lattice
for p, q being Element of L st L is I_Lattice holds
for b₄ being Element of L holds
( b₄ = p => q iff ( p "/\" b₄ [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b₄ ) ) );