assume A1: x = a ; :: thesis: |.x.| = |.a.|
per cases ( 0 <= x or 0 > x ) ;
suppose A2: 0 <= x ; :: thesis: |.x.| = |.a.|
hence |.x.| = a by A1, Def1
.= |.a.| by A2, A1, ABSVALUE:def 1 ;
:: thesis: verum
end;
suppose A3: 0 > x ; :: thesis: |.x.| = |.a.|
hence |.x.| = - x by Def1
.= - a by A1
.= |.a.| by A3, A1, ABSVALUE:def 1 ;
:: thesis: verum
end;
end;