let
x
be
Real
;
:: thesis:
(
x
^2
)
+
1
>
0
x
^2
>=
0
by
XREAL_1:63
;
hence
(
x
^2
)
+
1
>
0
;
:: thesis:
verum