ex x being set st x in dyadic 0 by XBOOLE_0:def 1;
hence not DYADIC is empty by Def4; :: thesis: verum