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 )
proof
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
proof
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;
Seg m c= Segm (m + 1) by AFINSQ_1:3;
then HWZSet1 r c= Segm (m + 1) by A2;
hence contradiction ; :: thesis: verum
end;
then consider n being Integer such that
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