let n be Nat; :: thesis: Triangle n = (n + 1) choose 2
(n + 1) choose 2 = (n * (n + 1)) / 2 by Th72;
hence Triangle n = (n + 1) choose 2 by Th19; :: thesis: verum