let c, d be Real; :: thesis: ( c > 0 implies (|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d) )

assume A1: c > 0 ; :: thesis: (|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d)

assume A2: (|.d.| + c) + 1 = - (((|.d.| + c) + c) + d) ; :: thesis: contradiction

assume A1: c > 0 ; :: thesis: (|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d)

assume A2: (|.d.| + c) + 1 = - (((|.d.| + c) + c) + d) ; :: thesis: contradiction