let p, q, p1 be Point of (TOP-REAL 2); :: thesis: ( p1 in LSeg (p,q) & p `2 = q `2 implies p1 `2 = q `2 )
assume p1 in LSeg (p,q) ; :: thesis: ( not p `2 = q `2 or p1 `2 = q `2 )
then consider r being Real such that
A1: p1 = ((1 - r) * p) + (r * q) and
0 <= r and
r <= 1 ;
assume A2: p `2 = q `2 ; :: thesis: p1 `2 = q `2
p1 `2 = (((1 - r) * p) `2) + ((r * q) `2) by A1, TOPREAL3:2
.= (((1 - r) * p) `2) + (r * (q `2)) by TOPREAL3:4
.= ((1 - r) * (p `2)) + (r * (q `2)) by TOPREAL3:4 ;
hence p1 `2 = q `2 by A2; :: thesis: verum