:: deftheorem Def5 defines /\/ FILTER_1:def 5 :
for L being Lattice
for F being Filter of L st L is I_Lattice holds
for b₃ being strict Lattice holds
( b₃ = L /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b₃ = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) );