let V be RealLinearSpace; :: thesis: for v, w being Point of V
for x being object st x in LSeg (v,w) holds
ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) )
let v, w be Point of V; :: thesis: for x being object st x in LSeg (v,w) holds
ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) )
let x be object ; :: thesis: ( x in LSeg (v,w) implies ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) ) )
assume x in LSeg (v,w) ; :: thesis: ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) )
then ex r being Real st
( x = ((1 - r) * v) + (r * w) & 0 <= r & r <= 1 ) ;
hence ex r being Real st
( 0 <= r & r <= 1 & x = ((1 - r) * v) + (r * w) ) ; :: thesis: verum