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