theorem Th6: :: DIOPHAN2:11

for r being irrational Real holds TRANQN .: (HWZSet r) = HWZSet1 r