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 set 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:18;
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 set st b₁ = 0 ) ; :: thesis: verum