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