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