:: deftheorem defines modular LATTICES:def 12 :
for IT being non empty LattStr holds
( IT is modular iff for a, b, c being Element of IT st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );