consider s being OperSymbol of S;
reconsider nt = Sym (s,V) as NonTerminal of (DTConMSA V) ;
consider p being SubtreeSeq of nt;
reconsider t = nt -tree p as Term of S,V ;
take t ; :: thesis: t . {} in [: the carrier' of S,{ the carrier of S}:]
nt = [s, the carrier of S] by MSAFREE:def 11;
then A1: [s, the carrier of S] = t . {} by TREES_4:def 4;
the carrier of S in { the carrier of S} by TARSKI:def 1;
hence t . {} in [: the carrier' of S,{ the carrier of S}:] by A1, ZFMISC_1:106; :: thesis: verum