let M be MidSp; for p, q, r, s being Point of M holds
( vect (p,q) = vect (r,s) iff p @ s = q @ r )
let p, q, r, s be Point of M; ( vect (p,q) = vect (r,s) iff p @ s = q @ r )
thus
( vect (p,q) = vect (r,s) implies p @ s = q @ r )
by MIDSP_1:37; ( p @ s = q @ r implies vect (p,q) = vect (r,s) )
thus
( p @ s = q @ r implies vect (p,q) = vect (r,s) )
verum