theorem :: TREES_1:52

for n, m being Nat holds not <*n*> is_a_proper_prefix_of <*m*> by Th2;