let p, q, r be FinSequence; :: thesis: ( p is_a_prefix_of r & q is_a_prefix_of r implies p,q are_c=-comparable )
assume A1: p is_a_prefix_of r ; :: thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable )
A2: ex p9 being FinSequence st r = p ^ p9 by A1, TREES_1:8;
assume A3: q is_a_prefix_of r ; :: thesis: p,q are_c=-comparable
A4: ex q9 being FinSequence st r = q ^ q9 by A3, TREES_1:8;
A5: ( len p <= len q or len q <= len p ) ;
A6: ( ex t being FinSequence st p ^ t = q or ex t being FinSequence st q ^ t = p ) by A2, A4, A5, FINSEQ_1:64;
thus ( p is_a_prefix_of q or q is_a_prefix_of p ) by A6, TREES_1:8; :: according to XBOOLE_0:def 9 :: thesis: verum