let x be Real; :: thesis: ( x in DYADIC implies for n being Element of NAT st inf_number_dyadic x <= n holds
x in dyadic n )
assume A1: x in DYADIC ; :: thesis: for n being Element of NAT st inf_number_dyadic x <= n holds
x in dyadic n
let n be Element of NAT ; :: thesis: ( inf_number_dyadic x <= n implies x in dyadic n )
assume A2: inf_number_dyadic x <= n ; :: thesis: x in dyadic n
A3: x in dyadic (inf_number_dyadic x) by A1, Th6;
dyadic (inf_number_dyadic x) c= dyadic n by A2, URYSOHN2:33;
hence x in dyadic n by A3; :: thesis: verum