theorem Th23: :: MIDSP_2:23
for M being MidSp
for p, q, r being Point of M holds
( p @ q = r iff vect (p,r) = vect (r,q) )