theorem Th19: :: MODAL_1:24

for Z being Tree
for x1, x2 being Element of Z st x1 = <*0*> & x2 = <*1*> & succ (Root Z) = {x1,x2} holds
Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))