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:6;
then 1 - r >= 1 - 1 by XREAL_1:21;
then A1: |.(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 RLVECT_1:def 8
.= dist (((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q))) by RLVECT_1:def 6
.= dist (((1 - r) * p),((1 - r) * q)) by Th21
.= (1 - r) * (dist (p,q)) by A1, Th26 ; :: thesis: verum