consider s being set such that
A1: s in the carrier of S and
A2: not X . s is empty by PBOOLE:def 15;
reconsider s = s as SortSymbol of S by A1;
consider x being Element of X . s;
root-tree [x,s] in the Sorts of (Free (S,X)) . s by A2, Th5;
hence not the Sorts of (Free (S,X)) is empty-yielding by PBOOLE:def 15; :: according to CATALG_1:def 3 :: thesis: verum