k mod l is Nat ;
hence k mod l is Element of NAT by ORDINAL1:def 12; :: thesis: verum