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