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