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