for G being non empty DTConstrStr
for t being set holds
( not t in TS G or ex d being Symbol of G st
( d in Terminals G & t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st
( o ==> roots p & t = o -tree p ) )