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
A2: ( p is_a_prefix_of s ^ r & s is_a_prefix_of p ^ q ) by A1, TREES_1:8;
thus p,s are_c=-comparable by A1, A2, TREES_2:1; :: thesis: verum