theorem Th2: :: TREES_1:3

for x, y being set st <*x*> is_a_prefix_of <*y*> holds
x = y