<*> D is Element of D * by FINSEQ_1:def 11;
hence ex b₁ being Element of D * st b₁ is empty ; :: thesis: verum