let n be Element of NAT ; :: thesis: for p, p1, p2 being Point of 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 ; :: 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 ex r1 being Real st
( p = ((1 - r1) * p1) + (r1 * p2) & 0 <= r1 & r1 <= 1 ) ;
hence ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) ) ; :: thesis: verum