let n be Element of NAT ; :: thesis: for p, q being Point of
for r being Real st r < 1 & p = ((1 - r) * q) + (r * p) holds
p = q
let p, q be Point of ; :: 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:22;
p = ((1 - (1 - r)) * p) + ((1 - r) * q) by A2;
hence p = q by A3, Th13; :: thesis: verum