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

proof

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

end;

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

proof

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

end;

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