let s be natural Number ; :: thesis: s choose s = 1
reconsider m = s - s as Element of NAT by INT_1:5;
m = 0 ;
then s choose s = s choose 0 by Th20;
hence s choose s = 1 by Th19; :: thesis: verum