thus ( L is satisfying_Bowden_inequality implies for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ) by LATTICES:def 3; :: thesis: ( ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ) implies L is satisfying_Bowden_inequality )
assume B1: for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ; :: thesis: L is satisfying_Bowden_inequality
let x, y, z be Element of L; :: according to LATQUASI:def 11 :: thesis: (x "\/" y) "/\" z [= x "\/" (y "/\" z)
(x "\/" (y "/\" z)) "\/" ((x "\/" y) "/\" z) = x "\/" (y "/\" z) by B1;
hence (x "\/" y) "/\" z [= x "\/" (y "/\" z) by LATTICES:def 3; :: thesis: verum