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 A1: ex q1 being FinSequence st
( q = q1 & q1 is_a_proper_prefix_of p ) by Def2;
assume r in ProperPrefixes p ; :: thesis: q,r are_c=-comparable
then A2: ex r1 being FinSequence st
( r = r1 & r1 is_a_proper_prefix_of p ) by Def2;
q is_a_prefix_of p by A1;
then consider n being Nat such that
A3: q = p | (Seg n) ;
r is_a_prefix_of p by A2;
then consider k being Nat such that
A4: r = p | (Seg k) ;
A5: ( 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:5;
then q = r | (Seg n) by A3, A4, FUNCT_1:51;
then q is_a_prefix_of r ;
hence q,r are_c=-comparable ; :: 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:5;
then r = q | (Seg k) by A3, A4, FUNCT_1:51;
then r is_a_prefix_of q ;
hence q,r are_c=-comparable ; :: thesis: verum
end;
hence q,r are_c=-comparable by A5; :: thesis: verum