let
r
be
Real
;
:: thesis:
(
r
<=
0
implies
.
r
.
=

r
)
assume
r
<=
0
;
:: thesis:
.
r
.
=

r
then
(
r
<
0
or
r
=
0
) ;
hence
.
r
.
=

r
by
Def1
;
:: thesis:
verum