for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence