let r be Real; :: thesis: for a being complex number st r >= 0 holds
angle (r,a) = Arg a
let a be complex number ; :: thesis: ( r >= 0 implies angle (r,a) = Arg a )
assume r >= 0 ; :: thesis: angle (r,a) = Arg a
then Arg r = 0 by Th23;
hence angle (r,a) = Arg (Rotate (a,(- 0))) by Def5
.= Arg a by Th19 ;
:: thesis: verum