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