n >= 1 + 1 by NAT_2:29;
then A1: n > 1 by NAT_1:13;
then n ^2 > n by SQUARE_1:14;
hence not n ^2 is trivial by NAT_2:28, A1; :: thesis: verum