let x be Real; :: thesis: ( x in DYADIC implies x in dyadic (inf_number_dyadic x) )
set s = inf_number_dyadic x;
defpred S₁[ Nat] means not x in dyadic (((inf_number_dyadic x) + 1) + $1);
assume A1: x in DYADIC ; :: thesis: x in dyadic (inf_number_dyadic x)
then consider k being Nat such that
A2: x in dyadic k by URYSOHN1:def 2;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: not x in dyadic (((inf_number_dyadic x) + 1) + i) ; :: thesis: S₁[i + 1]
assume x in dyadic (((inf_number_dyadic x) + 1) + (i + 1)) ; :: thesis: contradiction
then x in dyadic ((((inf_number_dyadic x) + 1) + i) + 1) ;
then (inf_number_dyadic x) + 0 = (inf_number_dyadic x) + (i + 2) by A1, A4, Def3;
hence contradiction ; :: thesis: verum

end;

assume A5: not x in dyadic (inf_number_dyadic x) ; :: thesis: contradiction
A6: inf_number_dyadic x < k

proof

assume not inf_number_dyadic x < k ; :: thesis: contradiction
then dyadic k c= dyadic (inf_number_dyadic x) by URYSOHN2:29;
hence contradiction by A5, A2; :: thesis: verum

end;

then consider i being Nat such that
A7: k = i + 1 by NAT_1:6;
inf_number_dyadic x <= i by A6, A7, NAT_1:13;
then consider m being Nat such that
A8: i = (inf_number_dyadic x) + m by NAT_1:10;
reconsider m = m as Nat ;
A9: S₁[ 0 ] by A1, A5, Def3;
for i being Nat holds S₁[i] from NAT_1:sch 2(A9, A3);
then not x in dyadic (((inf_number_dyadic x) + 1) + m) ;
hence contradiction by A2, A7, A8; :: thesis: verum