theorem Th1: :: TREES_A:1

for p, q, r, s being FinSequence st p ^ q = s ^ r holds
p,s are_c=-comparable