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 A1: x in ProperPrefixes p ; :: thesis: x is FinSequence
A2: ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) by A1, Def4;
thus x is FinSequence by A2; :: thesis: verum