let p, q, r be FinSequence; :: thesis: ( q ^ r in ProperPrefixes p implies q in ProperPrefixes p )
assume A1: q ^ r in ProperPrefixes p ; :: thesis: q in ProperPrefixes p
A2: q is_a_prefix_of q ^ r by Th1;
q ^ r is_a_proper_prefix_of p by A1, Th11;
then q is_a_proper_prefix_of p by A2, XBOOLE_1:59;
hence q in ProperPrefixes p by Th11; :: thesis: verum