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