consider x being set such that
A1: x in dyadic 0 by XBOOLE_0:def 1;
thus not DYADIC is empty by A1, Def4; :: thesis: verum