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 A1: p is_a_proper_prefix_of r ; :: thesis: ( not q is_a_prefix_of r or p,q are_c=-comparable )
A2: p is_a_prefix_of r by A1, XBOOLE_0:def 8;
thus ( not q is_a_prefix_of r or p,q are_c=-comparable ) by A2, Th1; :: thesis: verum