:: deftheorem defines EqRelLATT LATTICE5:def 1 :
for A being set holds EqRelLATT A = LattPOSet (EqRelLatt A);