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₁[ 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₁[s] ;
ex q being Nat st
( S₁[q] & ( for i being Nat st S₁[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;

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

per cases ( q = 0 or 0 < q ) ;

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

hence inf_number_dyadic x <= n by A2, A1, A4, Def3; :: thesis: verum

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

proof

assume x in dyadic m ; :: thesis: contradiction
then m + 1 <= m + 0 by A5, A7;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

hence inf_number_dyadic x <= n by A2, A1, A4, A6, A7, Def3; :: thesis: verum

end;

end;

end;

hence inf_number_dyadic x <= n ; :: thesis: verum