{} c= E ;
then {} in bool E by ZFMISC_1:def 1;
then {} is Subset of E by Def1;
hence ex b₁ being Subset of E st b₁ is empty ; :: thesis: verum