:: deftheorem defines LatOrder LATTAD_1:def 6 :
for L being non empty LattStr holds LatOrder L = { [a,b] where a, b is Element of L : a [= b } ;