theorem Th10: :: EUCLID:13

for n being Nat
for x1, x2 being Element of REAL n holds |.(x1 - x2).| <= |.x1.| + |.x2.|