{} is Element of Fin X by FINSUB_1:7;
hence ex b₁ being Element of Fin X st b₁ is empty ; :: thesis: verum