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