{} is Sequence of D by ORDINAL1:30;
hence ex b₁ being Sequence of D st b₁ is finite ; :: thesis: verum