let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real st r <= 1 holds
dist p,((r * p) + ((1 - r) * q)) = (1 - r) * (dist p,q)
let r be Real; :: thesis: ( r <= 1 implies dist p,((r * p) + ((1 - r) * q)) = (1 - r) * (dist p,q) )
assume r <= 1 ; :: thesis: dist p,((r * p) + ((1 - r) * q)) = (1 - r) * (dist p,q)
then 1 + r <= 1 + 1 by XREAL_1:8;
then 1 - r >= 1 - 1 by XREAL_1:23;
then A1: abs (1 - r) = 1 - r by ABSVALUE:def 1;
thus dist p,((r * p) + ((1 - r) * q)) = dist ((r + (1 - r)) * p),((r * p) + ((1 - r) * q)) by EUCLID:33
.= dist ((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q)) by EUCLID:37
.= dist ((1 - r) * p),((1 - r) * q) by Th21
.= (1 - r) * (dist p,q) by A1, Th26 ; :: thesis: verum