let z be Complex; :: thesis: ( 0 <= Arg z & Arg z < 2 * PI )
( ( 0 <= Arg z & Arg z < 2 * PI ) or z = 0 ) by Def1;
hence ( 0 <= Arg z & Arg z < 2 * PI ) by Def1, Lm6, Lm7; :: thesis: verum