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