let L be non empty join-commutative join-associative Huntington ComplLLattStr ; for a, b being Element of L holds a + ((b + (b `)) `) = a
let a, b be Element of L; a + ((b + (b `)) `) = a
set O = b + (b `);
A1:
((b + (b `)) `) ` = b + (b `)
by Th3;
A2: (b + (b `)) ` =
(((((b + (b `)) `) `) + (((b + (b `)) `) `)) `) + (((((b + (b `)) `) `) + ((b + (b `)) `)) `)
by Def6
.=
(((b + (b `)) + (b + (b `))) `) + ((b + (b `)) `)
by A1, Th4
;
A3:
b + (b `) = (a `) + a
by Th4;
b + (b `) =
(b + (b `)) + ((b + (b `)) `)
by Th4
.=
((b + (b `)) + ((b + (b `)) `)) + (((b + (b `)) + (b + (b `))) `)
by A2, LATTICES:def 5
.=
(b + (b `)) + (((b + (b `)) + (b + (b `))) `)
by Th4
;
then A4: (b + (b `)) + (b + (b `)) =
((b + (b `)) + (b + (b `))) + (((b + (b `)) + (b + (b `))) `)
by LATTICES:def 5
.=
b + (b `)
by Th4
;
hence a + ((b + (b `)) `) =
((((a `) + (a `)) `) + (((a `) + a) `)) + ((((a `) + a) `) + (((a `) + a) `))
by A2, A3, Def6
.=
(((a `) + (a `)) `) + ((((a `) + a) `) + (((a `) + a) `))
by A2, A4, A3, LATTICES:def 5
.=
a
by A2, A4, A3, Def6
;
verum