theorem Th1: :: SIN_COS2:1

for p, r being Real st p >= 0 & r >= 0 holds
p + r >= 2 * (sqrt (p * r))