let r be Real; :: thesis: |.r.| = |.r.|
reconsider rr = r as Real ;

per cases ( 0 <= r or r < 0 ) ;

suppose A1: 0 <= r ; :: thesis: |.r.| = |.r.|

then |.r.| = r by EXTREAL1:def 1;
hence |.r.| = |.r.| by A1, ABSVALUE:def 1; :: thesis: verum

end;

suppose A2: r < 0 ; :: thesis: |.r.| = |.r.|

then |.r.| = - r by EXTREAL1:def 1;
then |.rr.| = - rr ;
hence |.r.| = |.r.| by A2, ABSVALUE:def 1; :: thesis: verum

end;

end;