let r be irrational Real; :: thesis: for r1 being non negative Real ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r )

let r1 be non negative Real; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r )

0 < [\r1/] + 1 by INT_1:29;

then reconsider m = [\r1/] + 1 as Nat ;

ex n being Integer st

( n in HWZSet1 r & n > m )

A8: n in HWZSet1 r and

A9: n > m ;

ex n1 being Nat st

( n1 = n & ex p being Rational st

( p in HWZSet r & n1 = denominator p ) ) by A8;

hence ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r ) by A9; :: thesis: verum

( denominator q > [\r1/] + 1 & q in HWZSet r )

let r1 be non negative Real; :: thesis: ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r )

0 < [\r1/] + 1 by INT_1:29;

then reconsider m = [\r1/] + 1 as Nat ;

ex n being Integer st

( n in HWZSet1 r & n > m )

proof

then consider n being Integer such that
assume A1:
for n being Integer holds

( not n in HWZSet1 r or not n > m ) ; :: thesis: contradiction

A2: for n being Integer st n in HWZSet1 r holds

n in Seg m

then HWZSet1 r c= Segm (m + 1) by A2;

hence contradiction ; :: thesis: verum

end;( not n in HWZSet1 r or not n > m ) ; :: thesis: contradiction

A2: for n being Integer st n in HWZSet1 r holds

n in Seg m

proof

Seg m c= Segm (m + 1)
by AFINSQ_1:3;
let n be Integer; :: thesis: ( n in HWZSet1 r implies n in Seg m )

assume A3: n in HWZSet1 r ; :: thesis: n in Seg m

then n > 0 by Th10;

then A4: n + 0 >= 1 by NAT_1:19;

n <= m by A1, A3;

hence n in Seg m by A4; :: thesis: verum

end;assume A3: n in HWZSet1 r ; :: thesis: n in Seg m

then n > 0 by Th10;

then A4: n + 0 >= 1 by NAT_1:19;

n <= m by A1, A3;

hence n in Seg m by A4; :: thesis: verum

then HWZSet1 r c= Segm (m + 1) by A2;

hence contradiction ; :: thesis: verum

A8: n in HWZSet1 r and

A9: n > m ;

ex n1 being Nat st

( n1 = n & ex p being Rational st

( p in HWZSet r & n1 = denominator p ) ) by A8;

hence ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r ) by A9; :: thesis: verum