:: deftheorem Def9 defines join-absorbing LATTICES:def 9 :
for IT being non empty LattStr holds
( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a );