ex A being ManySortedSet of the carrier of S st {A} = the carrier of S --> {0} by Th5;
hence ( the Sorts of (Trivial_Algebra S) is finite-yielding & the Sorts of (Trivial_Algebra S) is non-empty ) by MSAFREE2:def 12; :: thesis: verum