let x be Real; :: thesis: ( x in DYADIC implies x in dyadic (inf_number_dyadic x) )
assume A1: x in DYADIC ; :: thesis: x in dyadic (inf_number_dyadic x)
set s = inf_number_dyadic x;
assume A2: not x in dyadic (inf_number_dyadic x) ; :: thesis: contradiction
consider k being Element of NAT such that
A3: x in dyadic k by A1, URYSOHN1:def 4;
A4: 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:33;
hence contradiction by A2, A3; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means not x in dyadic (((inf_number_dyadic x) + 1) + $1);
A5: S₁[ 0 ] by A1, A2, Def3;
A6: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: 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, A7, Def3;
hence contradiction ; :: thesis: verum

end;

A8: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A6);
consider i being Nat such that
A9: k = i + 1 by A4, NAT_1:6;
inf_number_dyadic x <= i by A4, A9, NAT_1:13;
then consider m being Nat such that
A10: i = (inf_number_dyadic x) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
not x in dyadic (((inf_number_dyadic x) + 1) + m) by A8;
hence contradiction by A3, A9, A10; :: thesis: verum