let r1, r2 be non negative Real; :: thesis: ( r1 * r2 = ((r1 + r2) / 2) ^2 iff r1 = r2 )

hereby :: thesis: ( r1 = r2 implies r1 * r2 = ((r1 + r2) / 2) ^2 )

assume r1 * r2 = ((r1 + r2) / 2) ^2 ; :: thesis: r1 = r2
then sqrt (r1 * r2) = (r1 + r2) / 2 by SQUARE_1:22;
hence r1 = r2 by Th19; :: thesis: verum

end;

thus ( r1 = r2 implies r1 * r2 = ((r1 + r2) / 2) ^2 ) ; :: thesis: verum