let n be 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 Nat st
( i <= 2 |^ n & x = i / (2 |^ n) ) by Def1;
hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def5; :: thesis: verum