let n be Nat; :: thesis: Triangle n <= Triangle (n + 1)
Triangle (n + 1) = (Triangle n) + (n + 1) by Th10;
hence Triangle n <= Triangle (n + 1) by NAT_1:16; :: thesis: verum