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 p is_a_prefix_of r ; :: thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable )
then A1: ex p9 being FinSequence st r = p ^ p9 by TREES_1:1;
assume q is_a_prefix_of r ; :: thesis: p,q are_c=-comparable
then A2: ex q9 being FinSequence st r = q ^ q9 by TREES_1:1;
( len p <= len q or len q <= len p ) ;
then ( ex t being FinSequence st p ^ t = q or ex t being FinSequence st q ^ t = p ) by A1, A2, FINSEQ_1:47;
hence ( p is_a_prefix_of q or q is_a_prefix_of p ) by TREES_1:1; :: according to XBOOLE_0:def 9 :: thesis: verum