( 0 in dyadic 0 & 1 in dyadic 0 ) by URYSOHN1:12;
hence ( 0 in DYADIC & 1 in DYADIC ) by URYSOHN1:def 4; :: thesis: verum