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 (TOP-REAL n) st An = ((1 - lambda) * x1) + (lambda * x2) & Bn = ((1 - mu) * x1) + (mu * x2) holds
Bn - An = (mu - lambda) * (x2 - x1)