thus uReal . 1 = uDyadic . 1 by Th46
.= 1_No by Th11, Def5 ; :: thesis: