consider X being V16() ManySortedSet of the carrier of S;
take FreeMSA X ; :: thesis: ( FreeMSA X is strict & FreeMSA X is non-empty & FreeMSA X is disjoint_valued )
thus ( FreeMSA X is strict & FreeMSA X is non-empty & FreeMSA X is disjoint_valued ) ; :: thesis: verum