thus the Sorts of (Free (S,X)) is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis:

proof

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

end;