per
cases
(
a
>=
0
or
a
<
0
)
;
suppose
A1
:
a
>=
0
;
:: thesis:
.
a
.
is
Element
of
NAT
then
.
a
.
=
a
by
ABSVALUE:def 1
;
hence
.
a
.
is
Element
of
NAT
by
A1
,
INT_1:3
;
:: thesis:
verum
end;
suppose
a
<
0
;
:: thesis:
.
a
.
is
Element
of
NAT
then
(
.
a
.
=

a
&

a
>
0
)
by
ABSVALUE:def 1
,
XREAL_1:58
;
hence
.
a
.
is
Element
of
NAT
by
INT_1:3
;
:: thesis:
verum
end;
end;