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

( 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