A1: not D in {{}} by TARSKI:def 1;
D in bool D by ZFMISC_1:def 1;
hence not BOOL D is empty by A1, XBOOLE_0:def 5; :: thesis: verum