let x be Real; :: thesis: ( x in DYADIC implies for n being Nat st inf_number_dyadic x <= n holds
x in dyadic n )
assume x in DYADIC ; :: thesis: for n being Nat st inf_number_dyadic x <= n holds
x in dyadic n
then A1: x in dyadic (inf_number_dyadic x) by Th5;
let n be Nat; :: thesis: ( inf_number_dyadic x <= n implies x in dyadic n )
assume inf_number_dyadic x <= n ; :: thesis: x in dyadic n
then dyadic (inf_number_dyadic x) c= dyadic n by URYSOHN2:29;
hence x in dyadic n by A1; :: thesis: verum