:: deftheorem defines vect MIDSP_1:def 10 :
for M being MidSp
for a, b being Element of M holds vect (a,b) = [a,b] ~ ;