per cases ( n >= k or n < k ) ;

suppose A1: n >= k ; :: thesis: n choose k is real

then reconsider l = n - k as Element of NAT by INT_1:18;
n choose k = (n ! ) / ((k ! ) * (l ! )) by A1, Def3;
hence n choose k is real ; :: thesis: verum

end;

suppose n < k ; :: thesis: n choose k is real

hence n choose k is real by Def3; :: thesis: verum

end;

end;