let n, m be Nat; :: thesis: for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable
let s be FinSequence of NAT ; :: thesis: ( n <> m implies not <*n*>,<*m*> ^ s are_c=-comparable )
assume A1: n <> m ; :: thesis: not <*n*>,<*m*> ^ s are_c=-comparable
assume A2: <*n*>,<*m*> ^ s are_c=-comparable ; :: thesis: contradiction

per cases ( <*n*> is_a_prefix_of <*m*> ^ s or <*m*> ^ s is_a_prefix_of <*n*> ) by A2;

suppose <*n*> is_a_prefix_of <*m*> ^ s ; :: thesis: contradiction

then A3: ex a being FinSequence st <*m*> ^ s = <*n*> ^ a by TREES_1:1;
m = (<*m*> ^ s) . 1 by FINSEQ_1:41
.= n by A3, FINSEQ_1:41 ;
hence contradiction by A1; :: thesis: verum

end;

suppose <*m*> ^ s is_a_prefix_of <*n*> ; :: thesis: contradiction

then consider a being FinSequence such that
A4: <*n*> = (<*m*> ^ s) ^ a by TREES_1:1;
n = ((<*m*> ^ s) ^ a) . 1 by A4
.= (<*m*> ^ (s ^ a)) . 1 by FINSEQ_1:32
.= m by FINSEQ_1:41 ;
hence contradiction by A1; :: thesis: verum

end;

end;