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, v1, v2 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) )
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 v0, v1, v2 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) )
assume A3: for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v2 "/\" v0) "\/" (v1 "/\" v0) ; :: thesis: for v0, v1, v2 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2)
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;

A11: 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 A7;
hence (v0 "/\" v1) "/\" v1 = v0 "/\" v1 by A2; :: thesis: verum

end;

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

proof

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

end;

A18: 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 A11;
hence (v0 "/\" v64) "\/" (v65 "/\" v64) = v64 "/\" (v65 "\/" (v0 "/\" v64)) by A3; :: thesis: verum

end;

A22: 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 A3;
hence v65 "/\" (v66 "\/" v64) = v65 "/\" (v66 "\/" (v64 "/\" v65)) by A18; :: thesis: verum

end;

A27: 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 A7;
hence v64 "/\" v64 = v64 "/\" ((v0 "/\" v64) "\/" v64) by A22; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A57: 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;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A101: 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 A57; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

A115: for v1, v65 being Element of L holds (v65 "/\" v1) "\/" (v1 "/\" v65) = v65 "/\" v1

proof

let v1, v65 be Element of L; :: thesis: (v65 "/\" v1) "\/" (v1 "/\" v65) = v65 "/\" v1
(v65 "/\" v1) "/\" v65 = v1 "/\" v65 by A86;
hence (v65 "/\" v1) "\/" (v1 "/\" v65) = v65 "/\" v1 by A105; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

let v0, v1, v2 be Element of L; :: thesis: (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2)
v0 "/\" (v1 "/\" v2) = (v1 "/\" v0) "/\" v2 by AA
.= (v0 "/\" v1) "/\" v2 by A2, A3, MeetCom ;
hence (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ; :: thesis: verum