theorem Th17: :: MODAL_1:22

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