let p, q, r be FinSequence; :: thesis: ( q in ProperPrefixes p & r in ProperPrefixes p implies q,r are_c=-comparable )
assume q in ProperPrefixes p ; :: thesis: ( not r in ProperPrefixes p or q,r are_c=-comparable )
then A2: ex q1 being FinSequence st
( q = q1 & q1 is_a_proper_prefix_of p ) by Def4;
assume r in ProperPrefixes p ; :: thesis: q,r are_c=-comparable
then A4: ex r1 being FinSequence st
( r = r1 & r1 is_a_proper_prefix_of p ) by Def4;
q is_a_prefix_of p by A2, XBOOLE_0:def 8;
then consider n being Element of NAT such that
A6: q = p | (Seg n) by Def1;
r is_a_prefix_of p by A4, XBOOLE_0:def 8;
then consider k being Element of NAT such that
A8: r = p | (Seg k) by Def1;
A9: ( n <= k implies q,r are_c=-comparable )

proof

assume n <= k ; :: thesis: q,r are_c=-comparable
then Seg n c= Seg k by FINSEQ_1:7;
then q = r | (Seg n) by A6, A8, FUNCT_1:82;
then q is_a_prefix_of r by Def1;
hence q,r are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

( k <= n implies q,r are_c=-comparable )

proof

assume k <= n ; :: thesis: q,r are_c=-comparable
then Seg k c= Seg n by FINSEQ_1:7;
then r = q | (Seg k) by A6, A8, FUNCT_1:82;
then r is_a_prefix_of q by Def1;
hence q,r are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

hence q,r are_c=-comparable by A9; :: thesis: verum