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 4;
hence ( p @ q = r iff vect p,r = vect r,q ) by Th25; :: thesis: verum