{} is XFinSequence of D by Th14;
hence ex b₁ being XFinSequence of D st b₁ is empty ; :: thesis: verum