:: deftheorem defines LattRel FILTER_1:def 8 :
for L being Lattice holds LattRel L = { [p,q] where p, q is Element of L : p [= q } ;