let n, m, k be Element of NAT ; :: thesis: ( n <= m implies (m --> k) | n = n --> k )
assume n <= m ; :: thesis: (m --> k) | n = n --> k
then n c= m by NAT_1:40;
then n /\ m = n by XBOOLE_1:28;
hence (m --> k) | n = n --> k by FUNCOP_1:18; :: thesis: verum