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
then <*n*> is_a_prefix_of <*m*> by XBOOLE_0:def 8;
hence contradiction by A1, Th16; :: thesis: verum