theorem Th11: :: TREES_1:12

for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )