{} NAT is without_zero by PSCOMP_1:def 1;
hence ex b₁ being Subset of NAT st
( b₁ is empty & b₁ is without_zero & b₁ is finite ) ; :: thesis: verum