theorem Th1: :: CAYLDICK:1

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