:: deftheorem Def9 defines + MIDSP_1:def 9 :
for M being MidSp
for u, v, b₄ being Vector of M holds
( b₄ = u + v iff ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b₄ = [(p `1),(q `2)] ~ ) );