theorem :: RLTOPSP1:69

for V being RealLinearSpace
for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)