theorem Th137: :: RVSUM_1:137

for n being Nat
for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|