theorem :: EUCLID_6:41

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