the Sorts of T is GeneratorSet of T by MSAFREE2:6;
hence not for b₁ being GeneratorSet of T holds b₁ is V5() ; :: thesis: verum