let r be Integer; :: thesis: ( r > 2 implies 1 / (r ^2) <= 1 / 9 )
assume r > 2 ; :: thesis: 1 / (r ^2) <= 1 / 9
then r >= 2 + 1 by NAT_1:13;
then r ^2 >= 3 * 3 by XREAL_1:66;
hence 1 / (r ^2) <= 1 / 9 by XREAL_1:85; :: thesis: verum