let x be Element of X; :: thesis: x is Element of D
X in bool D by Def2;
then A1: X c= D by ZFMISC_1:def 1;
x in X by Def2;
then x in D by A1, TARSKI:def 3;
hence x is Element of D by Def2; :: thesis: verum