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