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