theorem :: SERIES_5:9

for x, y being Real holds x + y <= sqrt (2 * ((x ^2) + (y ^2)))