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) "/\" (v0 "\/" 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) "/\" (v0 "\/" 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) "/\" (v0 "\/" 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;

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

proof

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

end;

A15: 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 = v0 "/\" (v1 "/\" v1) by A2, A3, MeetAssoc
.= v0 "/\" v1 by A2, A3, Lemma1 ;
hence (v0 "/\" v1) "/\" v1 = v0 "/\" v1 ; :: thesis: verum

end;

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

end;

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

proof

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

end;

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

proof

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

end;

A39: 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 A22; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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