consider x being Element of X;
{x} is Subset of X by SUBSET_1:63;
then {x} is Element of Fin X by FINSUB_1:def 5;
hence not for b₁ being Element of Fin X holds b₁ is empty ; :: thesis: verum