set G = the non-empty finite-yielding ManySortedSubset of the Sorts of A;
take GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A ; :: thesis: ( GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is strict & GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is finitely-generated )
thus ( GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is strict & GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the non-empty finite-yielding ManySortedSubset of the Sorts of A is finitely-generated ) ; :: thesis: verum