let p, q, r, s be FinSequence; :: thesis: ( p ^ q = s ^ r implies p,s are_c=-comparable )
assume A1: p ^ q = s ^ r ; :: thesis: p,s are_c=-comparable
then ( p is_a_prefix_of s ^ r & s is_a_prefix_of p ^ q ) by TREES_1:1;
hence p,s are_c=-comparable by A1, TREES_2:1; :: thesis: verum