let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in DYADIC or x in [.0,1.] )
assume A1: x in DYADIC ; :: thesis: x in [.0,1.]
then reconsider x = x as Real ;
A2: ex n being Nat st x in dyadic n by A1, URYSOHN1:def 2;
reconsider x = x as R_eal by XXREAL_0:def 1;
( 0 <= x & x <= 1 ) by A2, URYSOHN1:1;
hence x in [.0,1.] by XXREAL_1:1; :: thesis: verum