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