theorem Th40: :: MIDSP_1:40

for M being MidSp
for a, b, c being Element of M holds (vect (a,b)) + (vect (b,c)) = vect (a,c)