let d be Dyadic; :: thesis: ex n being Nat st uDyadic . d in Day n

per cases ( d >= 0 or d < 0 ) ;

suppose d >= 0 ; :: thesis: ex n being Nat st uDyadic . d in Day n

hence ex n being Nat st uDyadic . d in Day n by Lm6; :: thesis: verum

end;

suppose d < 0 ; :: thesis: ex n being Nat st uDyadic . d in Day n

then consider n being Nat such that
A1: uDyadic . (- d) in Day n by Lm6;
take n ; :: thesis: uDyadic . d in Day n
uDyadic . (- d) = - (uDyadic . d) by Th27;
then - (- (uDyadic . d)) in Day n by A1, SURREALR:11;
hence uDyadic . d in Day n ; :: thesis: verum

end;

end;