let x be Real; :: thesis: for n being Nat st x in dyadic n holds

inf_number_dyadic x <= n

let n be Nat; :: thesis: ( x in dyadic n implies inf_number_dyadic x <= n )

A1: dyadic n c= DYADIC by URYSOHN2:23;

defpred S_{1}[ Nat] means x in dyadic $1;

assume A2: x in dyadic n ; :: thesis: inf_number_dyadic x <= n

then A3: ex s being Nat st S_{1}[s]
;

ex q being Nat st

( S_{1}[q] & ( for i being Nat st S_{1}[i] holds

q <= i ) ) from NAT_1:sch 5(A3);

then consider q being Nat such that

A4: x in dyadic q and

A5: for i being Nat st x in dyadic i holds

q <= i ;

A6: q <= n by A2, A5;

inf_number_dyadic x <= n

let n be Nat; :: thesis: ( x in dyadic n implies inf_number_dyadic x <= n )

A1: dyadic n c= DYADIC by URYSOHN2:23;

defpred S

assume A2: x in dyadic n ; :: thesis: inf_number_dyadic x <= n

then A3: ex s being Nat st S

ex q being Nat st

( S

q <= i ) ) from NAT_1:sch 5(A3);

then consider q being Nat such that

A4: x in dyadic q and

A5: for i being Nat st x in dyadic i holds

q <= i ;

A6: q <= n by A2, A5;

now :: thesis: ( ( q = 0 & inf_number_dyadic x <= n ) or ( 0 < q & inf_number_dyadic x <= n ) )end;

hence
inf_number_dyadic x <= n
; :: thesis: verumper cases
( q = 0 or 0 < q )
;

end;

case
0 < q
; :: thesis: inf_number_dyadic x <= n

then consider m being Nat such that

A7: q = m + 1 by NAT_1:6;

reconsider m = m as Nat ;

not x in dyadic m

end;A7: q = m + 1 by NAT_1:6;

reconsider m = m as Nat ;

not x in dyadic m

proof

hence
inf_number_dyadic x <= n
by A2, A1, A4, A6, A7, Def3; :: thesis: verum
assume
x in dyadic m
; :: thesis: contradiction

then m + 1 <= m + 0 by A5, A7;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then m + 1 <= m + 0 by A5, A7;

hence contradiction by XREAL_1:6; :: thesis: verum