let M be MidSp; :: thesis: for p, q, r being Point of M holds
( p @ q = r iff vect (p,r) = vect (r,q) )
let p, q, r be Point of M; :: thesis: ( p @ q = r iff vect (p,r) = vect (r,q) )
( p @ q = r iff p @ q = r @ r ) by MIDSP_1:def 3;
hence ( p @ q = r iff vect (p,r) = vect (r,q) ) by Th22; :: thesis: verum