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