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