set x = the Element of X;
{ the Element of X} is Subset of X by SUBSET_1:41;
then { the Element of 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