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