theorem Th4: :: NAT_6:4

for n being natural even number holds n div 2 = n / 2