:: deftheorem defines HWZSet1 DIOPHAN2:def 3 :
for r being irrational Real holds HWZSet1 r = { x where x is Nat : ex p being Rational st
( p in HWZSet r & x = denominator p ) } ;