theorem :: EUCLID_2:27

for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 - q2))| = |(p,q1)| - |(p,q2)| by Th22;