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