consider X being V5() ManySortedSet of ;
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