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 free )
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 free ) ; :: thesis: verum