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