let s, t be natural Number ; :: thesis: ( s >= 1 & t = s - 1 implies s choose t = s )
assume that
A1: s >= 1 and
A2: t = s - 1 ; :: thesis: s choose t = s
s choose t = s choose 1 by A1, A2, Th20;
hence s choose t = s by A1, Th23; :: thesis: verum