for T, T9 being DecoratedTree
for x being set st ( not x in rng T or not x in Leaves T ) holds
(T,x) <- T9 = T