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 v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 )
assume A2:
L is join-absorbing
; ( ex v0, v2, v1 being Element of L st not v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) or for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 )
assume A3:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0)
; for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0
A7:
for v65, v66 being Element of L holds v65 = (v66 "/\" v65) "\/" (v65 "/\" v65)
A51:
for v1, v0 being Element of L holds (v0 "/\" v1) "\/" v1 = v1
A74:
for v64, v65 being Element of L holds (v65 "/\" v64) "\/" v65 = v65
let v1, v0 be Element of L; v0 "\/" (v0 "/\" v1) = v0
(v0 "/\" v1) "\/" v0 = v0
by A74;
hence
v0 "\/" (v0 "/\" v1) = v0
by A2, A3, JoinCom; verum