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 being Element of L holds v0 "/\" v0 = 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 v0 being Element of L holds v0 "/\" v0 = v0 )
assume A3:
for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0)
; for v0 being Element of L holds v0 "/\" v0 = v0
A7:
for v65, v66 being Element of L holds v65 = (v66 "/\" v65) "\/" (v65 "/\" v65)
A11:
for v1, v0 being Element of L holds (v0 "/\" v1) "/\" v1 = v0 "/\" v1
A18:
for v65, v64, v0 being Element of L holds (v0 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" (v65 "\/" (v0 "/\" v64))
A35:
for v65, v64, v66 being Element of L holds v65 "/\" (v66 "\/" v64) = v65 "/\" (v66 "\/" (v64 "/\" v65))
A40:
for v64, v0 being Element of L holds v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64)
A49:
for v64, v65 being Element of L holds (v64 "/\" v64) "\/" ((v65 "/\" v64) "/\" v64) = v64 "/\" v64
A51:
for v64, v65 being Element of L holds (v64 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" v64
let v65 be Element of L; v65 "/\" v65 = v65
(v65 "/\" v65) "\/" (v65 "/\" v65) = v65
by A7;
hence
v65 "/\" v65 = v65
by A51; verum