let M be MidSp; :: thesis: M, vectgroup M are_associated_wrp vect M
let p be Point of M; :: according to MIDSP_2:def 2 :: thesis: for q, r being Point of M holds
( p @ q = r iff (vect M) . p,r = (vect M) . r,q )
let q, r be Point of M; :: thesis: ( p @ q = r iff (vect M) . p,r = (vect M) . r,q )
set w = vect M;
( (vect M) . p,r = vect p,r & (vect M) . r,q = vect r,q ) by Def8;
hence ( p @ q = r iff (vect M) . p,r = (vect M) . r,q ) by Th26; :: thesis: verum