let p, q, r be FinSequence; :: thesis: ( p is_a_proper_prefix_of r & q is_a_prefix_of r implies p,q are_c=-comparable )
assume p is_a_proper_prefix_of r ; :: thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable )
then p is_a_prefix_of r by XBOOLE_0:def 8;
hence ( not q is_a_prefix_of r or p,q are_c=-comparable ) by Th1; :: thesis: verum