theorem :: SQUARE_1:59

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