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