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 v64, v2, v1 being Element of L holds (v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (v1 "/\" (v64 "/\" (v1 "\/" v2))) = v64 "/\" (v1 "\/" v2)

proof

let v64, v2, v1 be Element of L; :: thesis: (v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (v1 "/\" (v64 "/\" (v1 "\/" v2))) = v64 "/\" (v1 "\/" v2)
(v64 "/\" (v1 "\/" v2)) "/\" (v1 "\/" v2) = (v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (v1 "/\" (v64 "/\" (v1 "\/" v2))) by A3;
hence (v2 "/\" (v64 "/\" (v1 "\/" v2))) "\/" (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, v1, v66 being Element of L holds v66 "\/" (v65 "/\" (v66 "\/" v1)) = (v66 "\/" v1) "/\" (v65 "\/" v66)

proof

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

end;

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

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

proof

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

end;

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

proof

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

end;

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

A40: 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 A35; :: thesis: verum

end;

A49: 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 A40; :: thesis: verum

end;

A51: 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 A49; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

A111: 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 A2, A3, MeetCom
.= (v64 "/\" v64) "/\" v65 by MeetAssoc, A2, A3
.= v64 "/\" v65 by A2, A3, Lemma1
.= v65 "/\" v64 by MeetCom, A2, A3 ;
hence v64 "/\" (v65 "/\" v64) = v65 "/\" v64 ; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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