for M being MidSp
for W being ATLAS of M holds
( ( for a being Point of M
for x being Vector of W ex b being Point of M st W . (a,b) = x ) & ( for a, b, c being Point of M st W . (a,b) = W . (a,c) holds
b = c ) & ( for a, b, c being Point of M holds (W . (a,b)) + (W . (b,c)) = W . (a,c) ) )