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 v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0 )
assume A2: L is join-absorbing ; :: thesis: ( 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) ; :: thesis: 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)

proof

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

end;

A51: for v1, v0 being Element of L holds (v0 "/\" v1) "\/" v1 = v1

proof

let v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" v1 = v1
v1 "/\" v1 = v1 by A2, A3, Lemma1;
hence (v0 "/\" v1) "\/" v1 = v1 by A7; :: thesis: verum

end;

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

proof

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

end;

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