let
x
be
ExtReal
;
:: thesis:
(
.
x
.
=

x
&
x
<>
0
implies
x
<
0
)
reconsider
x
=
x
as
R_eal
by
XXREAL_0:def 1
;
0
<=
.
x
.
;
hence
(
.
x
.
=

x
&
x
<>
0
implies
x
<
0
) ;
:: thesis:
verum