-infty
<>
+infty
by
TARSKI:def 2
,
Lm1
;
hence
-infty
<
+infty
by
Def5
,
Lm4
,
Lm6
;
:: thesis:
verum