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