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