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