:: deftheorem Def7 defines Vector MIDSP_1:def 7 :
for M being MidSp
for b₂ being non empty Subset of [: the carrier of M, the carrier of M:] holds
( b₂ is Vector of M iff ex p being Element of [: the carrier of M, the carrier of M:] st b₂ = p ~ );