{ the set } is finite by Lm1;
hence ex b₁ being set st
( not b₁ is empty & b₁ is finite ) ; :: thesis: verum