for i, n being Nat
for p being Point of (TOP-REAL n) st i in Seg n holds
(Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i)))