theorem Th2: :: MODAL_1:3

for n, m being Nat
for s being FinSequence of NAT st n <> m holds
not <*n*> is_a_proper_prefix_of <*m*> ^ s