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