:: deftheorem defines QLT-selfmodular LATQUASI:def 13 :
for L being non empty LattStr holds
( L is QLT-selfmodular iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) );