let M be MidSp; :: thesis: 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; :: thesis: ( 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:57; :: thesis: ( p @ s = q @ r implies vect p,q = vect r,s )
thus ( p @ s = q @ r implies vect p,q = vect r,s ) :: thesis: verum

proof

assume p @ s = q @ r ; :: thesis: vect p,q = vect r,s
then p,q @@ r,s by MIDSP_1:def 5;
then [p,q] ## [r,s] by MIDSP_1:31;
hence vect p,q = vect r,s by MIDSP_1:56; :: thesis: verum

end;