let
a
be
ExtReal
;
:: thesis:
(
-infty
>=
a
implies
a
=
-infty
)
a
>=
-infty
by
Def5
,
Lm4
,
Lm6
;
hence
(
-infty
>=
a
implies
a
=
-infty
)
by
Th1
;
:: thesis:
verum