:: deftheorem defines vector MIDSP_2:def 7 :
for M being MidSp
for p, q being Point of M holds vector (p,q) = vect (p,q);