let x be R_eal; :: thesis: for a being Real st x = a holds
|.x.| = abs a
let a be Real; :: thesis: ( x = a implies |.x.| = abs a )
assume A1: x = a ; :: thesis: |.x.| = abs a

per cases ( 0 <= x or not 0 <= x ) ;

suppose A2: 0 <= x ; :: thesis: |.x.| = abs a

then |.x.| = a by A1, EXTREAL1:def 3;
hence |.x.| = abs a by A1, A2, ABSVALUE:def 1; :: thesis: verum

end;

suppose A3: not 0 <= x ; :: thesis: |.x.| = abs a

then |.x.| = - x by EXTREAL1:37
.= - a by A1, SUPINF_2:3 ;
hence |.x.| = abs a by A1, A3, ABSVALUE:def 1; :: thesis: verum

end;

end;