assume
A1
:
r
"
<=
0
;
:: according to
XXREAL_0:def 6
:: thesis:
contradiction
(
r
"
)
"
>
0
by
XXREAL_0:def 6
;
then
(
(
r
"
)
*
(
(
r
"
)
"
)
=
1 &
(
r
"
)
*
(
(
r
"
)
"
)
<=
0
)
by
A1
,
Lm20
,
XCMPLX_0:def 7
;
hence
contradiction
by
Lm4
,
Lm8
;
:: thesis:
verum