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