( 1 --> 0 <> {} & 1 --> 0 is dominated_by_0 ) by Lm3;
hence ex b₁ being XFinSequence of st
( not b₁ is empty & b₁ is dominated_by_0 ) ; :: thesis: verum