theorem Th53: :: TREES_3:53

for p being FinSequence st p is Tree-yielding holds
elementary_tree (len p) c= tree p