let n be Nat; :: thesis: Triangle n >= 0
A1: Triangle n = (n * (n + 1)) / 2 by Th19;
thus Triangle n >= 0 by A1; :: thesis: verum