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