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