:: deftheorem Def2 defines mod NAT_D:def 2 :
for k, l being natural Number
for b₃ being Nat holds
( b₃ = k mod l iff ( ex t being Nat st
( k = (l * t) + b₃ & b₃ < l ) or ( b₃ = 0 & l = 0 ) ) );