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:37; :: 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 4;
then [p,q] ## [r,s] by MIDSP_1:19;
hence vect (p,q) = vect (r,s) by MIDSP_1:36; :: thesis: verum
end;