for M being MidSp
for W being ATLAS of M
for a, b, c being Point of M holds
( a @ c = b iff W . (a,c) = Double (W . (a,b)) )