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:5;
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;