let
r
be
Real
;
:: thesis:
0
<=
r
+
.
r
.
A1
:
0
<=
.
r
.
by
COMPLEX1:46
;
(
.
r
.
+
.
r
.
=
r
+
.
r
.
or
.
r
.
+
r
=
(

r
)
+
r
)
by
Def1
;
hence
0
<=
r
+
.
r
.
by
A1
;
:: thesis:
verum