theorem Th32: :: TREES_9:32

for n being Nat
for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )