:: deftheorem Def1 defines TS DTCONSTR:def 1 :
for G being non empty DTConstrStr
for b₂ being Subset of (FinTrees the carrier of G) holds
( b₂ = TS G iff ( ( for d being Symbol of G st d in Terminals G holds
root-tree d in b₂ ) & ( for o being Symbol of G
for p being FinSequence of b₂ st o ==> roots p holds
o -tree p in b₂ ) & ( for F being Subset of (FinTrees the carrier of G) st ( for d being Symbol of G st d in Terminals G holds
root-tree d in F ) & ( for o being Symbol of G
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
b₂ c= F ) ) );