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

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