let r be Real; :: thesis: for a being Complex st r >= 0 holds
angle (r,a) = Arg a
let a be Complex; :: thesis: ( r >= 0 implies angle (r,a) = Arg a )
assume r >= 0 ; :: thesis: angle (r,a) = Arg a
then Arg r = 0 by COMPTRIG:35;
hence angle (r,a) = Arg (Rotate (a,(- 0))) by Def3
.= Arg a by COMPTRIG:62 ;
:: thesis: verum