let p1, p, q 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:7
.= (((1 - r) * p) `2 ) + (r * (q `2 )) by TOPREAL3:9
.= ((1 - r) * (p `2 )) + (r * (q `2 )) by TOPREAL3:9 ;
hence p1 `2 = q `2 by A2; :: thesis: verum