the Sorts of T is GeneratorSet of T by MSAFREE2:6;
hence not for b₁ being GeneratorSet of T holds b₁ is non-empty ; :: thesis: verum