let p, q be FinSequence; :: thesis: ( p in ProperPrefixes q implies len p < len q )
assume p in ProperPrefixes q ; :: thesis: len p < len q
then p is_a_proper_prefix_of q by Th36;
hence len p < len q by Th24; :: thesis: verum