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