theorem :: TREES_4:21

for x, y being object holds x -flat_tree <*y*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,(root-tree y))