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