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