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