thus ( n >= k implies ex r1 being set st
for l being Nat st l = n - k holds
r1 = (n !) / ((k !) * (l !)) ) :: thesis: ( not n >= k implies ex b₁ being number st b₁ = 0 )

proof

assume n >= k ; :: thesis: ex r1 being set st
for l being Nat st l = n - k holds
r1 = (n !) / ((k !) * (l !))
then reconsider m = n - k as Element of NAT by INT_1:5;
take (n !) / ((k !) * (m !)) ; :: thesis: for l being Nat st l = n - k holds
(n !) / ((k !) * (m !)) = (n !) / ((k !) * (l !))
thus for l being Nat st l = n - k holds
(n !) / ((k !) * (m !)) = (n !) / ((k !) * (l !)) ; :: thesis: verum

end;

thus ( not n >= k implies ex b₁ being number st b₁ = 0 ) ; :: thesis: verum