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;