let
x
be
Real
;
:: thesis:
(
sgn
x
=
1 implies
0
<
x
)
assume
that
A1
:
sgn
x
=
1
and
A2
:
0
>=
x
;
:: thesis:
contradiction
(
x
<
0
or
x
=
0
)
by
A2
;
hence
contradiction
by
A1
,
Def2
;
:: thesis:
verum