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