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

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