let
n
be
Nat
;
:: thesis:
for
p
being
Point
of
(
TOP-REAL
n
)
holds
0
<=
|.
p
.|
let
p
be
Point
of
(
TOP-REAL
n
)
;
:: thesis:
0
<=
|.
p
.|
(
|.
p
.|
=
sqrt
|(
p
,
p
)|
&
0
<=
|(
p
,
p
)|
)
by
Th33
,
Th35
;
hence
0
<=
|.
p
.|
by
SQUARE_1:def 2
;
:: thesis:
verum