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