let
a
,
b
be
Real
;
:: thesis:
0
<=
(
a
^2
)
+
(
b
^2
)
(
0
<=
a
^2
&
0
<=
b
^2
)
by
XREAL_1:63
;
then
0
+
0
<=
(
a
^2
)
+
(
b
^2
)
;
hence
0
<=
(
a
^2
)
+
(
b
^2
)
;
:: thesis:
verum