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

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

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

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

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