let x be set ; :: thesis: for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence
let p be FinSequence; :: thesis: ( x in ProperPrefixes p implies x is FinSequence )
assume x in ProperPrefixes p ; :: thesis: x is FinSequence
then ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) by Def4;
hence x is FinSequence ; :: thesis: verum