:: deftheorem defines LatRelStr LATTAD_1:def 12 :
for L being GAD_Lattice holds LatRelStr L = RelStr(# the carrier of L,(LatOrder L) #);