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 9;
hence (1 / 2) * (v + w) in LSeg v,w ; :: thesis: verum