theorem :: TREES_3:43

for T, T9 being Tree
for p being FinSequence of NAT st p in Leaves T holds
T c= T with-replacement (p,T9)