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 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