let n be Element of NAT ; :: thesis: dyadic n c= DYADIC
for x being set st x in dyadic n holds
x in DYADIC by URYSOHN1:def 2;
hence dyadic n c= DYADIC by TARSKI:def 3; :: thesis: verum