let r be irrational Real; :: thesis: for h being Nat st h in HWZSet1 r holds
h > 0
let h be Nat; :: thesis: ( h in HWZSet1 r implies h > 0 )
assume h in HWZSet1 r ; :: thesis: h > 0
then ex h1 being Nat st
( h1 = h & ex p being Rational st
( p in HWZSet r & h1 = denominator p ) ) ;
hence h > 0 ; :: thesis: verum