consider s being object 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, Th4;
hence the Sorts of (Free (S,X)) is empty-yielding ; :: according to CATALG_1:def 2 :: thesis: verum