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