:: deftheorem ModRedef defines modular LATQUASI:def 14 :
for L being non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr holds
( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) );