consider x being Element of NAT ;
{x} is IL-Subset of S by Def1;
hence not for b₁ being IL-Subset of S holds b₁ is empty ; :: thesis: verum