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;