Description: Closure of squaring in reals, deduction form. (Contributed by Mario Carneiro, 28-May-2016)