let a be real number ; :: thesis: ( a >= 0 implies |.a.| = a )
A1: a in REAL by XREAL_0:def 1;
then A2: Im a = 0 by Def3;
assume a >= 0 ; :: thesis: |.a.| = a
then Re a >= 0 by A1, Def2;
hence |.a.| = Re a by A2, SQUARE_1:22
.= a by A1, Def2 ;
:: thesis: verum