let
x
be
ExtReal
;
:: thesis:
(
x
<=
0
implies
.
x
.
=

x
)
assume
A1
:
x
<=
0
;
:: thesis:
.
x
.
=

x
per
cases
(
x
<
0
or
x
=
0
)
by
A1
;
suppose
x
<
0
;
:: thesis:
.
x
.
=

x
hence
.
x
.
=

x
by
Def1
;
:: thesis:
verum
end;
suppose
A2
:
x
=
0
;
:: thesis:
.
x
.
=

x
then

0
=

x
;
hence
.
x
.
=

x
by
A2
,
Def1
;
:: thesis:
verum
end;
end;