:: deftheorem Def12 defines [# FILTER_2:def 12 :
for L being Lattice
for p, q being Element of L st p [= q holds
[#p,q#] = { r where r is Element of L : ( p [= r & r [= q ) } ;