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