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

( 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;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