:: deftheorem Def6 defines SubtreeSeq DTCONSTR:def 6 :
for G being non empty with_nonterminals with_useful_nonterminals DTConstrStr
for nt being NonTerminal of G
for b₃ being FinSequence of TS G holds
( b₃ is SubtreeSeq of nt iff nt ==> roots b₃ );