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