let n, s be Nat; :: thesis: Polygon (s,n) = ((s - 2) * (Triangle (n -' 1))) + n
Polygon (s,n) = ((s - 2) * ((n * (n - 1)) / 2)) + n
.= ((s - 2) * (Triangle (n -' 1))) + n by Th21 ;
hence Polygon (s,n) = ((s - 2) * (Triangle (n -' 1))) + n ; :: thesis: verum