:: deftheorem defines ThetaOrder LATTAD_1:def 7 :
for L being non empty LattStr holds ThetaOrder L = { [a,b] where a, b is Element of L : a "/\" b = b } ;