let x be Real; :: thesis: ( x in DYADIC implies x in dyadic )
set s = inf_number_dyadic x;
defpred S1[ Nat] means not x in dyadic (( + 1) + \$1);
assume A1: x in DYADIC ; :: thesis:
then consider k being Nat such that
A2: x in dyadic k by URYSOHN1:def 2;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: not x in dyadic (( + 1) + i) ; :: thesis: S1[i + 1]
assume x in dyadic (( + 1) + (i + 1)) ; :: thesis: contradiction
then x in dyadic ((( + 1) + i) + 1) ;
then (inf_number_dyadic x) + 0 = + (i + 2) by A1, A4, Def3;
hence contradiction ; :: thesis: verum
end;
assume A5: not x in dyadic ; :: thesis: contradiction
A6: inf_number_dyadic x < k
proof end;
then consider i being Nat such that
A7: k = i + 1 by NAT_1:6;
inf_number_dyadic x <= i by ;
then consider m being Nat such that
A8: i = + m by NAT_1:10;
reconsider m = m as Nat ;
A9: S1[ 0 ] by A1, A5, Def3;
for i being Nat holds S1[i] from NAT_1:sch 2(A9, A3);
then not x in dyadic (( + 1) + m) ;
hence contradiction by A2, A7, A8; :: thesis: verum