thus uReal . 0 = uDyadic . 0 by Th46
.= uInt . 0 by Def5
.= 0_No by Def1 ; :: thesis: