theorem Th7: :: BORSUK_7:7

for r being Real st sin r = 0 holds
ex i being Integer st r = PI * i