let s be Nat; :: 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 Th30;
hence s choose s = 1 by Th29; :: thesis: verum