let x be Real; :: thesis: for n being Element of NAT st x in dyadic n holds
inf_number_dyadic x <= n
let n be Element of NAT ; :: thesis: ( x in dyadic n implies inf_number_dyadic x <= n )
assume A1: x in dyadic n ; :: thesis: inf_number_dyadic x <= n
A2: dyadic n c= DYADIC by URYSOHN2:27;
defpred S₁[ Nat] means x in dyadic $1;
A3: ex s being Nat st S₁[s] by A1;
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 & ( for i being Nat st x in dyadic i holds
q <= i ) ) ;
A5: q <= n by A1, A4;

now

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

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

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

end;

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

then consider m being Nat such that
A6: q = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
not x in dyadic m

proof

assume x in dyadic m ; :: thesis: contradiction
then m + 1 <= m + 0 by A4, A6;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

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

end;

end;

end;

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