theorem Th133: :: MSAFREE5:142

for t, t1 being DecoratedTree
for xi, nu being Node of t st not xi c= nu & not nu c= xi holds
(t with-replacement (xi,t1)) | nu = t | nu