theorem Th71: :: NUMPOLY1:71

for x being number holds
( x in SquareNumbers iff x is square )