set s = the OperSymbol of S;
reconsider nt = Sym ( the OperSymbol of S,V) as NonTerminal of (DTConMSA V) ;
set p = the SubtreeSeq of nt;
reconsider t = nt -tree the SubtreeSeq of nt as Term of S,V ;
take t ; :: thesis: t . {} in [: the carrier' of S,{ the carrier of S}:]
nt = [ the OperSymbol of S, the carrier of S] by MSAFREE:def 9;
then A1: [ the OperSymbol of 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:87; :: thesis: verum