let n be Element of NAT ; :: thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 holds
ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) )
let p, p1, p2 be Point of (TOP-REAL n); :: thesis: ( p in LSeg p1,p2 implies ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) ) )
assume p in LSeg p1,p2 ; :: thesis: ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) )
then p in { (((1 - r) * p1) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r1 being Real such that
A1: ( p = ((1 - r1) * p1) + (r1 * p2) & 0 <= r1 & r1 <= 1 ) ;
thus ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) ) by A1; :: thesis: verum