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