let n be Nat; :: thesis: ( n |^ 3 <= 98 implies n <= 4 )
assume A1: n |^ 3 <= 98 ; :: thesis: n <= 4
A2: n |^ 3 = (n * n) * n by POLYEQ_5:2;
assume n > 4 ; :: thesis: contradiction
then A3: n >= 4 + 1 by NAT_1:13;
then n * n >= 5 * 5 by XREAL_1:66;
then (n * n) * n >= 25 * 5 by A3, XREAL_1:66;
hence contradiction by A1, A2, XXREAL_0:2; :: thesis: verum