let r, s, t be natural Number ; :: thesis: ( s >= t & r = s - t implies s choose t = s choose r )
assume A1: s >= t ; :: thesis: ( not r = s - t or s choose t = s choose r )
t - s >= 0 - s by XREAL_1:9;
then A2: - (- s) >= - (t - s) by XREAL_1:24;
assume A3: r = s - t ; :: thesis: s choose t = s choose r
then t = s - r ;
then s choose r = (s !) / ((r !) * (t !)) by A2, Def3;
hence s choose t = s choose r by A1, A3, Def3; :: thesis: verum