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 )

proof

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;

assume B1: for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) ; :: thesis: 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