let n, m be Element of NAT ; :: thesis: not <*n*> is_a_proper_prefix_of <*m*>
assume A1: <*n*> is_a_proper_prefix_of <*m*> ; :: thesis: contradiction
A2: <*n*> is_a_prefix_of <*m*> by A1, XBOOLE_0:def 8;
thus contradiction by A1, A2, Th16; :: thesis: verum