let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)

for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

let p, q be Point of (TOP-REAL n); :: thesis: for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

let r be Real; :: thesis: ( r < 1 & p = ((1 - r) * q) + (r * p) implies p = q )

assume that

A1: r < 1 and

A2: p = ((1 - r) * q) + (r * p) ; :: thesis: p = q

set s = 1 - r;

r + 0 < 1 by A1;

then A3: 0 < 1 - r by XREAL_1:20;

p = ((1 - (1 - r)) * p) + ((1 - r) * q) by A2;

hence p = q by A3, Th3; :: thesis: verum

for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

let p, q be Point of (TOP-REAL n); :: thesis: for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds

p = q

let r be Real; :: thesis: ( r < 1 & p = ((1 - r) * q) + (r * p) implies p = q )

assume that

A1: r < 1 and

A2: p = ((1 - r) * q) + (r * p) ; :: thesis: p = q

set s = 1 - r;

r + 0 < 1 by A1;

then A3: 0 < 1 - r by XREAL_1:20;

p = ((1 - (1 - r)) * p) + ((1 - r) * q) by A2;

hence p = q by A3, Th3; :: thesis: verum