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