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 being Element of L holds v0 "\/" v1 = v1 "\/" v0 )
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 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)
; for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0
A8:
for v65, v66 being Element of L holds v65 = (v66 "/\" v65) "\/" (v65 "/\" v65)
A12:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" v1 = v0 "/\" v1
A15:
for v65, v64, v0 being Element of L holds (v0 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" (v65 "\/" (v0 "/\" v64))
A19:
for v65, v64, v66 being Element of L holds v65 "/\" (v66 "\/" v64) = v65 "/\" (v66 "\/" (v64 "/\" v65))
A24:
for v64, v0 being Element of L holds v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64)
A29:
for v64, v65 being Element of L holds (v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64) = v64 "/\" v64
A31:
for v64, v65 being Element of L holds (v64 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" v64
A42:
for v64, v65 being Element of L holds v64 "/\" (v65 "\/" v64) = v64
A46:
for v2, v1 being Element of L holds (v2 "/\" (v1 "\/" v2)) "\/" (v1 "/\" (v1 "\/" v2)) = v1 "\/" v2
A48:
for v2, v1 being Element of L holds v2 "\/" (v1 "/\" (v1 "\/" v2)) = v1 "\/" v2
let v1, v2 be Element of L; v1 "\/" v2 = v2 "\/" v1
v1 "/\" (v1 "\/" v2) = v1
by A3;
hence
v1 "\/" v2 = v2 "\/" v1
by A48; verum