let L be non empty LattStr ; :: thesis: ( L is join-absorbing & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ) implies for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0 )
assume A3: L is join-absorbing ; :: thesis: ( ex v0, v2, v1 being Element of L st not v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) or for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0 )
assume A4: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ; :: thesis: for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0
A53: for v2, v0 being Element of L holds v0 "/\" (v2 "\/" v2) = v2 "/\" v0

proof

let v2, v0 be Element of L; :: thesis: v0 "/\" (v2 "\/" v2) = v2 "/\" v0
(v2 "/\" v0) "\/" (v2 "/\" v0) = v0 "/\" (v2 "\/" v2) by A4;
hence v0 "/\" (v2 "\/" v2) = v2 "/\" v0 by A3, A4, JoinIdem; :: thesis: verum

end;

let v2, v0 be Element of L; :: thesis: v2 "/\" v0 = v0 "/\" v2
v2 "\/" v2 = v2 by A3, A4, JoinIdem;
hence v2 "/\" v0 = v0 "/\" v2 by A53; :: thesis: verum