let n be Element of NAT ; :: thesis: for x being Element of dyadic n holds
( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )
let x be Element of dyadic n; :: thesis: ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )
ex i being Element of NAT st
( i <= 2 |^ n & x = i / (2 |^ n) ) by Def3;
hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def7; :: thesis: verum