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