theorem Th2: :: NUMPOLY1:2

for n being even Integer holds n / 2 is Integer