let a be Real; :: thesis: ( a >= 0 implies |.a.| = a )
assume a >= 0 ; :: thesis: |.a.| = a
then Re a >= 0 by Def1;
hence |.a.| = Re a by SQUARE_1:22
.= a by Def1 ;
:: thesis: verum