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