let L be non empty ComplLattStr ; :: thesis: ( L is join-commutative & L is join-associative & L is Robbins implies L is satisfying_DN_1 )
assume A1: ( L is join-commutative & L is join-associative & L is Robbins ) ; :: thesis: L is satisfying_DN_1
then reconsider L' = L as non empty join-commutative join-associative Robbins ComplLattStr ;
A2: L' is Huntington ;
let x, y, z, u be Element of L; :: according to ROBBINS2:def 1 :: thesis: (((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` = z
A3: (((x + y) ` ) + z) *' z = (z + ((x + y) ` )) *' z by A1, LATTICES:def 4
.= z *' (z + ((x + y) ` )) by A1, ROBBINS1:8
.= z by A2, ROBBINS1:22 ;
A4: (z + x) *' (z + (x ` )) = z by A2, Th58;
A5: ((((x + y) ` ) + z) *' x) + z = z + ((((x + y) ` ) + z) *' x) by A1, LATTICES:def 4
.= (z + (((x + y) ` ) + z)) *' (z + x) by A2, ROBBINS1:32
.= ((((x + y) ` ) + z) + z) *' (z + x) by A2, LATTICES:def 4
.= (((x + y) ` ) + (z + z)) *' (z + x) by A2, 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) by A2, LATTICES:def 4
.= ((z + (x ` )) *' (z + (y ` ))) *' (z + x) by A2, ROBBINS1:32
.= (z + x) *' ((z + (x ` )) *' (z + (y ` ))) by A2, ROBBINS1:8
.= (z + x) *' (((x ` ) + z) *' (z + (y ` ))) by A2, LATTICES:def 4
.= (z + x) *' (((x ` ) + z) *' ((y ` ) + z)) by A2, LATTICES:def 4
.= ((z + x) *' ((x ` ) + z)) *' ((y ` ) + z) by A2, ROBBINS1:17
.= ((z + x) *' (z + (x ` ))) *' ((y ` ) + z) by A2, LATTICES:def 4
.= z *' (z + (y ` )) by A2, A4, LATTICES:def 4
.= 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, A3, A5, ROBBINS1:18 ;
hence (((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` = z ; :: thesis: verum