consider A being ManySortedSet of such that
A1: {A} = the carrier of S --> {0 } by Th6;
thus ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty ) by A1, MSAFREE2:def 12; :: thesis: verum