theorem Th12: :: METRIC_3:12

for a, b, c, d being Real st 0 <= a & 0 <= b & 0 <= c & 0 <= d holds
sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))