let p, q be FinSequence; :: thesis: ( p in ProperPrefixes q iff p is_a_proper_prefix_of q )
thus ( p in ProperPrefixes q implies p is_a_proper_prefix_of q ) :: thesis: ( p is_a_proper_prefix_of q implies p in ProperPrefixes q )

proof

assume p in ProperPrefixes q ; :: thesis: p is_a_proper_prefix_of q
then ex r being FinSequence st
( p = r & r is_a_proper_prefix_of q ) by Def2;
hence p is_a_proper_prefix_of q ; :: thesis: verum

end;

thus ( p is_a_proper_prefix_of q implies p in ProperPrefixes q ) by Def2; :: thesis: verum