theorem
Th1
:
:: EUCLID12:1
for
n
being
Nat
for
lambda
,
mu
being
Real
for
x1
,
x2
being
Element
of
REAL
n
for
An
,
Bn
being
Point
of
(
TOPREAL
n
)
st
An
=
(
(
1

lambda
)
*
x1
)
+
(
lambda
*
x2
)
&
Bn
=
(
(
1

mu
)
*
x1
)
+
(
mu
*
x2
)
holds
Bn

An
=
(
mu

lambda
)
*
(
x2

x1
)