let L be non empty join-commutative join-associative ComplLLattStr ; :: thesis: ( L is Robbins implies L is satisfying_DN_1 )
assume L is Robbins ; :: thesis: L is satisfying_DN_1
then reconsider L9 = L as non empty join-commutative join-associative Robbins ComplLLattStr ;
let x, y, z, u be Element of L; :: according to ROBBINS2:def 1 :: thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z
A2: L9 is Huntington ;
then A3: (z + x) *' (z + (x `)) = z by Th58;
A4: (((x + y) `) + z) *' z = (z + ((x + y) `)) *' z
.= z *' (z + ((x + y) `))
.= z by A2, ROBBINS1:22 ;
A5: ((((x + y) `) + z) *' x) + z = z + ((((x + y) `) + z) *' x)
.= (z + (((x + y) `) + z)) *' (z + x) by A2, ROBBINS1:32
.= ((((x + y) `) + z) + z) *' (z + x)
.= (((x + y) `) + (z + z)) *' (z + x) by LATTICES:def 5
.= (((x + y) `) + z) *' (z + x) by A2, ROBBINS1:13
.= (((((x `) *' (y `)) `) `) + z) *' (z + x) by A2, ROBBINS1:18
.= (((x `) *' (y `)) + z) *' (z + x) by A2, ROBBINS1:3
.= (z + ((x `) *' (y `))) *' (z + x)
.= ((z + (x `)) *' (z + (y `))) *' (z + x) by A2, ROBBINS1:32
.= (z + x) *' ((z + (x `)) *' (z + (y `)))
.= (z + x) *' (((x `) + z) *' (z + (y `)))
.= (z + x) *' (((x `) + z) *' ((y `) + z))
.= ((z + x) *' ((x `) + z)) *' ((y `) + z) by A2, ROBBINS1:17
.= ((z + x) *' (z + (x `))) *' ((y `) + z)
.= z *' (z + (y `)) by A3
.= z by A2, ROBBINS1:22 ;
(((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = (((((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + u) `)) `)) `) `)) `) ` by A2, ROBBINS1:18
.= (((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + u) `)) `)) `) `) by A2, ROBBINS1:3
.= (((((x + y) `) + z) `) `) *' (x + (((z `) + ((z + u) `)) `)) by A2, ROBBINS1:3
.= (((x + y) `) + z) *' (x + (((z `) + ((z + u) `)) `)) by A2, ROBBINS1:3
.= (((((x + y) `) `) *' (z `)) `) *' (x + (((z `) + ((z + u) `)) `)) by A2, ROBBINS1:18
.= (((x + y) *' (z `)) `) *' (x + (((z `) + ((z + u) `)) `)) by A2, ROBBINS1:3
.= (((x + y) *' (z `)) `) *' (x + (((((z `) `) *' (((z + u) `) `)) `) `)) by A2, ROBBINS1:18
.= (((x + y) *' (z `)) `) *' (x + (((z *' (((z + u) `) `)) `) `)) by A2, ROBBINS1:3
.= (((x + y) *' (z `)) `) *' (x + (z *' (((z + u) `) `))) by A2, ROBBINS1:3
.= (((x + y) *' (z `)) `) *' (x + (z *' (z + u))) by A2, ROBBINS1:3
.= (((x + y) *' (z `)) `) *' (x + z) by A2, ROBBINS1:22
.= ((((x + y) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) by A2, ROBBINS1:31
.= ((((((x + y) `) `) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) by A2, ROBBINS1:3
.= ((((x + y) `) + z) *' x) + ((((x + y) *' (z `)) `) *' z) by A2, ROBBINS1:18
.= ((((x + y) `) + z) *' x) + ((((((x + y) `) `) *' (z `)) `) *' z) by A2, ROBBINS1:3
.= z by A2, A4, A5, ROBBINS1:18 ;
hence (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z ; :: thesis: verum