let A be MSAlgebra over S; :: thesis: ( A is X,S -terms implies A is disjoint_valued )
assume A is X,S -terms ; :: thesis: A is disjoint_valued
then the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) ;
hence the Sorts of A is disjoint_valued ; :: according to MSAFREE1:def 2 :: thesis: verum