let x be ExtReal; :: thesis: for a being Real st x = a holds
|.x.| = |.a.|
let a be Real; :: thesis: ( x = a implies |.x.| = |.a.| )
assume A1: x = a ; :: thesis: |.x.| = |.a.|
reconsider x = x as R_eal by XXREAL_0:def 1;

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

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

then |.x.| = a by A1, Def1;
hence |.x.| = |.a.| by ABSVALUE:def 1; :: thesis: verum

end;

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

then |.x.| = - x by Def1
.= - a by A1, SUPINF_2:2 ;
hence |.x.| = |.a.| by A1, A2, ABSVALUE:def 1; :: thesis: verum

end;

end;