theorem Th12: :: TREES_1:13

for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q by Th11, Th5;