theorem :: TREES_3:41

for T being Tree holds T is T-Substitution of 0