theorem Th19: :: DIOPHAN2:2

for r1, r2 being non negative Real holds
( sqrt (r1 * r2) = (r1 + r2) / 2 iff r1 = r2 )