let m be Element of NAT ; :: thesis: {} is_a_proper_prefix_of <*m*>
{} is_a_prefix_of <*m*> by XBOOLE_1:2;
hence {} is_a_proper_prefix_of <*m*> by XBOOLE_0:def 8; :: thesis: verum