{} NAT is IL-Subset of S by Def1;
hence ex b₁ being IL-Subset of S st b₁ is empty ; :: thesis: verum