E in bool E by ZFMISC_1:def 1;
hence E is Subset of E by Def2; :: thesis: verum