for p1, p2 being Point of (TOP-REAL 2) holds
( (p1 + p2) `1 = (p1 `1) + (p2 `1) & (p1 + p2) `2 = (p1 `2) + (p2 `2) )