let z be complex number ; :: thesis: ( Arg z = 0 iff ( Re z >= 0 & Im z = 0 ) )
A1: |.z.| = |.z.| + (0 * <i> ) ;

hereby :: thesis: ( Re z >= 0 & Im z = 0 implies Arg z = 0 )

assume Arg z = 0 ; :: thesis: ( Re z >= 0 & Im z = 0 )
then z = |.z.| by Th24;
then ( Re z = |.z.| & Im z = 0 ) by A1, COMPLEX1:28;
hence ( Re z >= 0 & Im z = 0 ) by COMPLEX1:132; :: thesis: verum

end;

assume A2: ( Re z >= 0 & Im z = 0 ) ; :: thesis: Arg z = 0
then z = (Re z) + (0 * <i> ) by COMPLEX1:29;
hence Arg z = 0 by A2, COMPTRIG:53; :: thesis: verum