:: deftheorem defines LatRelStr LATWAL_2:def 5 :
for L being WA_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);