let
n
be
Nat
;
:: thesis:
for
x
,
y
being
Element
of
REAL
n
holds
|.
|(
x
,
y
)|
.|
<=
|.
x
.|
*
|.
y
.|
let
x
,
y
be
Element
of
REAL
n
;
:: thesis:
|.
|(
x
,
y
)|
.|
<=
|.
x
.|
*
|.
y
.|
(
len
x
=
n
&
len
y
=
n
)
by
CARD_1:def 7
;
hence
|.
|(
x
,
y
)|
.|
<=
|.
x
.|
*
|.
y
.|
by
EUCLID_2:15
;
:: thesis:
verum