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