theorem Th31: :: FILTER_1:31

for L being Lattice
for p, q being Element of L holds
( [p,q] in LattRel L iff p [= q )