( {1} is Subset of NAT & not 0 in {1} ) ;
hence ex b₁ being Subset of NAT st
( not b₁ is empty & b₁ is without_zero & b₁ is finite ) ; :: thesis: verum