theorem :: MIDSP_1:37

for M being MidSp
for a, b, c, d being Element of M st vect (a,b) = vect (c,d) holds
a @ d = b @ c by Th29;