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

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