theorem Th7: :: DIOPHAN2:12

for r being irrational Real st HWZSet r is finite holds
HWZSet1 r is finite