let V be RealLinearSpace; :: thesis: for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)
let v, w be Point of V; :: thesis: (1 / 2) * (v + w) in LSeg (v,w)
(1 / 2) * (v + w) = ((1 - (1 / 2)) * v) + ((1 / 2) * w) by RLVECT_1:def 5;
hence (1 / 2) * (v + w) in LSeg (v,w) ; :: thesis: verum