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

proof

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

end;

A79: for v66, v64, v65 being Element of L holds (v65 "/\" v64) "\/" (v66 "/\" v65) = v65 "/\" (v64 "\/" v66)

proof

let v66, v64, v65 be Element of L; :: thesis: (v65 "/\" v64) "\/" (v66 "/\" v65) = v65 "/\" (v64 "\/" v66)
v64 "/\" v65 = v65 "/\" v64 by A3, A4, MeetCom;
hence (v65 "/\" v64) "\/" (v66 "/\" v65) = v65 "/\" (v64 "\/" v66) by A72; :: thesis: verum

end;

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