theorem Th9: :: INT_5:9

for a being Integer
for m being Nat holds a ^2 is_quadratic_residue_mod m