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 v0 being Element of L holds v0 "\/" v0 = v0 )
assume A3: L is join-absorbing ; :: thesis: ( 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 A4: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ; :: thesis: for v0 being Element of L holds v0 "\/" v0 = v0
A8: 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 A3;
hence v65 = (v66 "/\" v65) "\/" (v65 "/\" v65) by A4; :: thesis: verum

end;

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

proof

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

end;

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

proof

let v65, v64, v0 be Element of L; :: thesis: (v0 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" (v65 "\/" (v0 "/\" v64))
(v0 "/\" v64) "/\" v64 = v0 "/\" v64 by A12;
hence (v0 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" (v65 "\/" (v0 "/\" v64)) by A4; :: thesis: verum

end;

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

proof

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

end;

A24: for v64, v0 being Element of L holds v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64)

proof

let v64, v0 be Element of L; :: thesis: v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64)
(v0 "/\" v64) "\/" (v64 "/\" v64) = v64 by A8;
hence v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64) by A19; :: thesis: verum

end;

A35: for v64, v1 being Element of L holds (v64 "/\" v64) "\/" (((v1 "/\" v64) "\/" v64) "/\" ((v1 "/\" v64) "\/" v64)) = (v1 "/\" v64) "\/" v64

proof

let v64, v1 be Element of L; :: thesis: (v64 "/\" v64) "\/" (((v1 "/\" v64) "\/" v64) "/\" ((v1 "/\" v64) "\/" v64)) = (v1 "/\" v64) "\/" v64
v64 "/\" ((v1 "/\" v64) "\/" v64) = v64 "/\" v64 by A24;
hence (v64 "/\" v64) "\/" (((v1 "/\" v64) "\/" v64) "/\" ((v1 "/\" v64) "\/" v64)) = (v1 "/\" v64) "\/" v64 by A8; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

A46: 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 A3, A4, Lemma1;
hence (v0 "/\" v1) "\/" v1 = v1 by A8; :: thesis: verum

end;

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

proof

let v0, v1 be Element of L; :: thesis: v0 "\/" v0 = (v1 "/\" v0) "\/" v0
(v1 "/\" v0) "\/" v0 = v0 by A46;
hence v0 "\/" v0 = (v1 "/\" v0) "\/" v0 by A44; :: thesis: verum

end;

now :: thesis: for v0, v1 being Element of L holds v0 "\/" v0 = v0

let v0, v1 be Element of L; :: thesis: v0 "\/" v0 = v0
(v1 "/\" v0) "\/" v0 = v0 by A46;
hence v0 "\/" v0 = v0 by A48; :: thesis: verum

end;

hence for v0 being Element of L holds v0 "\/" v0 = v0 ; :: thesis: verum