for o being object st o in DYADIC holds
o is rational by Def3;
hence ( DYADIC is rational-membered & not DYADIC is empty ) by Def3, MEMBERED:def 4; :: thesis: verum