let d be Dyadic; :: thesis: ( d >= 0 implies ex n being Nat st uDyadic . d in Day n )
assume A1: d >= 0 ; :: thesis: ex n being Nat st uDyadic . d in Day n

per cases ( d is Integer or not d is Integer ) ;

suppose d is Integer ; :: thesis: ex n being Nat st uDyadic . d in Day n

then reconsider n = d as Element of NAT by A1, INT_1:3;
( uDyadic . d = uInt . n & uInt . n in Day n ) by Def5, Th1;
hence ex n being Nat st uDyadic . d in Day n ; :: thesis: verum

end;

suppose d is not Integer ; :: thesis: ex n being Nat st uDyadic . d in Day n

then consider n, m, p being Nat such that
A2: ( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) ) by A1, Th28;
born (uDyadic . d) = (n + (p + 1)) + 1 by A2, Th26;
then uDyadic . d in Day ((n + (p + 1)) + 1) by SURREAL0:def 18;
hence ex n being Nat st uDyadic . d in Day n ; :: thesis: verum

end;

end;