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 )

thus
( r1 = r2 implies r1 * r2 = ((r1 + r2) / 2) ^2 )
; :: thesis: verumassume
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;then sqrt (r1 * r2) = (r1 + r2) / 2 by SQUARE_1:22;

hence r1 = r2 by Th19; :: thesis: verum