consider s being set such that
A1: s in the carrier of S and
A2: not X . s is empty by PBOOLE:def 12;
reconsider s = s as SortSymbol of S by A1;
set x = the Element of X . s;
root-tree [ the Element of X . s,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 12; :: according to CATALG_1:def 2 :: thesis: verum