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