let r, s be Real; :: thesis: ( not |.r.| = |.s.| or r = s or r = - s )

assume A1: |.r.| = |.s.| ; :: thesis: ( r = s or r = - s )

assume A2: r <> s ; :: thesis: r = - s

assume A1: |.r.| = |.s.| ; :: thesis: ( r = s or r = - s )

assume A2: r <> s ; :: thesis: r = - s