:: deftheorem Def3 defines choose NEWTON:def 3 :
for k, n being natural Number
for b₃ being number holds
( ( n >= k implies ( b₃ = n choose k iff for l being Nat st l = n - k holds
b₃ = (n !) / ((k !) * (l !)) ) ) & ( not n >= k implies ( b₃ = n choose k iff b₃ = 0 ) ) );