theorem Th9: :: EUCLID:12

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