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