:: deftheorem defines - MIDSP_1:def 11 :
for M being MidSp
for u, b₃ being Vector of M holds
( b₃ = - u iff u + b₃ = ID M );