x ^2 is Element of NAT by INT_1:3, XREAL_1:63;
hence x ^2 is natural ; :: thesis: verum