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 ( [s,the carrier of S] = t . {} & the carrier of S in {the carrier of S} ) by TARSKI:def 1, TREES_4:def 4;
hence t . {} in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:106; :: thesis: verum