theorem Th7: :: TREES_1:8

for x being set
for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2 ^ <*x*>