set v = the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));
take A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #); :: thesis: A is X,S -terms
thus the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis: verum

proof

thus the Sorts of A c= the Sorts of (Free (S,X)) ; :: according to PBOOLE:def 18 :: thesis: verum

end;