theorem Th9: :: TREES_A:9

for T, T1 being Tree
for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)