theorem :: MIDSP_1:36

for M being MidSp
for a, b, c, d being Element of M st [a,b] ## [c,d] holds
vect (a,b) = vect (c,d) by Th27;