thus
( L is satisfying_QLT1 implies for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) )
:: thesis: ( ( for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) ) implies L is satisfying_QLT1 )

let v0, v2, v1 be Element of L; :: according to LATQUASI:def 1 :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)

(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by B1, LATTICES:def 3;

hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis: verum

proof

assume B1:
for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2)
; :: thesis: L is satisfying_QLT1
assume A1:
L is satisfying_QLT1
; :: thesis: for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2)

let v0, v1, v2 be Element of L; :: thesis: v0 "/\" v1 [= v0 "/\" (v1 "\/" v2)

(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by A1;

hence v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) by LATTICES:def 3; :: thesis: verum

end;let v0, v1, v2 be Element of L; :: thesis: v0 "/\" v1 [= v0 "/\" (v1 "\/" v2)

(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by A1;

hence v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) by LATTICES:def 3; :: thesis: verum

let v0, v2, v1 be Element of L; :: according to LATQUASI:def 1 :: thesis: (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2)

(v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) by B1, LATTICES:def 3;

hence (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ; :: thesis: verum