let a, b be Complex; :: thesis: ( a <> 0 & b <> 0 & Arg a = Arg b implies Arg (- a) = Arg (- b) )
assume ( a <> 0 & b <> 0 & Arg a = Arg b ) ; :: thesis: Arg (- a) = Arg (- b)
then Arg (Rotate (a,PI)) = Arg (Rotate (b,PI)) by Th60;
then Arg (- a) = Arg (Rotate (b,PI)) by Th58;
hence Arg (- a) = Arg (- b) by Th58; :: thesis: verum