theorem Th20: :: MODAL_1:25

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