theorem Th1: :: MODAL_1:1

for n, m being Nat
for s being FinSequence of NAT st n <> m holds
not <*n*>,<*m*> ^ s are_c=-comparable