let
x
be
ExtReal
;
:: thesis:
(
x
<>
0
implies
0
<
.
x
.
)
assume
A1
:
x
<>
0
;
:: thesis:
0
<
.
x
.
per
cases
(
0
<=
x
or not
0
<=
x
)
;
suppose
0
<=
x
;
:: thesis:
0
<
.
x
.
hence
0
<
.
x
.
by
A1
,
Def1
;
:: thesis:
verum
end;
suppose
A2
: not
0
<=
x
;
:: thesis:
0
<
.
x
.
then
0
<

x
;
hence
0
<
.
x
.
by
A2
,
Def1
;
:: thesis:
verum
end;
end;