let
x
be
ExtReal
;
:: thesis:
(
x
+
x
=
0
implies
x
=
0
)
assume
x
+
x
=
0
;
:: thesis:
x
=
0
then
x
=

x
by
XXREAL_3:8
;
hence
x
=
0
by
Th1
;
:: thesis:
verum