let d be Dyadic; :: thesis: ( 0 <= d iff 0_No <= uDyadic . d )
( 0_No = uInt . 0 & uInt . 0 = uDyadic . 0 ) by Def1, Def5;
hence ( 0 <= d iff 0_No <= uDyadic . d ) by Th24; :: thesis: verum