let x be Real; :: thesis: ( x in DYADIC implies x in dyadic (inf_number_dyadic x) )

set s = inf_number_dyadic x;

defpred S_{1}[ 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_{1}[i] holds

S_{1}[i + 1]

A6: inf_number_dyadic x < k

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_{1}[ 0 ]
by A1, A5, Def3;

for i being Nat holds S_{1}[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

set s = inf_number_dyadic x;

defpred S

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

S

proof

assume A5:
not x in dyadic (inf_number_dyadic x)
; :: thesis: contradiction
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: not x in dyadic (((inf_number_dyadic x) + 1) + i) ; :: thesis: S_{1}[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 A4: not x in dyadic (((inf_number_dyadic x) + 1) + i) ; :: thesis: S

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

A6: inf_number_dyadic x < k

proof

then consider i being Nat such that
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 dyadic k c= dyadic (inf_number_dyadic x) by URYSOHN2:29;

hence contradiction by A5, A2; :: thesis: verum

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

for i being Nat holds S

then not x in dyadic (((inf_number_dyadic x) + 1) + m) ;

hence contradiction by A2, A7, A8; :: thesis: verum