for M being MidSp
for W being Element of setvect M ex T being Element of setvect M st W + T = ID M