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 b1 being number st b1 = 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 b1 being number st b1 = 0 ) ; :: thesis: verum