let L be non empty LattStr ; ( 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
; ( 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)
; 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)
A79:
for v66, v64, v65 being Element of L holds (v65 "/\" v64) "\/" (v66 "/\" v65) = v65 "/\" (v64 "\/" v66)
let v0, v1, v2 be Element of L; 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)
; verum