consider p being Prime;
p |^ 2 divides 0 by NAT_D:6;
hence 0 is square-containing by Def1; :: thesis: verum