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