let a be Real; :: thesis: ( a >= 0 implies |.a.| = a )
A1: a in REAL by XREAL_0:def 1;
assume a >= 0 ; :: thesis: |.a.| = a
then Re a >= 0 by A1, Def1;
hence |.a.| = Re a by SQUARE_1:22
.= a by Def1 ;
:: thesis: verum