let V be RealLinearSpace; :: thesis: for v, w being Point of V holds v in LSeg v,w
let v, w be Point of V; :: thesis: v in LSeg v,w
v = (1 - 0 ) * v by RLVECT_1:def 11
.= ((1 - 0 ) * v) + (0. V) by RLVECT_1:10
.= ((1 - 0 ) * v) + (0 * w) by RLVECT_1:23 ;
hence v in LSeg v,w ; :: thesis: verum