{} in Fin X by FINSUB_1:7;
then {{}} is Subset of (Fin X) by ZFMISC_1:31;
hence not for b₁ being Subset of (Fin X) holds b₁ is empty ; :: thesis: verum