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

x
implies
x
=
0
)
per
cases
(
x
=
+infty
or
x
=
infty
or
x
in
REAL
)
by
XXREAL_0:14
;
suppose
(
x
=
+infty
or
x
=
infty
) ;
:: thesis:
(
x
=

x
implies
x
=
0
)
hence
(
x
=

x
implies
x
=
0
) ;
:: thesis:
verum
end;
suppose
x
in
REAL
;
:: thesis:
(
x
=

x
implies
x
=
0
)
then
reconsider
y
=
x
as
Element
of
REAL
;

x
=

y
by
XXREAL_3:def 3
;
hence
(
x
=

x
implies
x
=
0
) ;
:: thesis:
verum
end;
end;