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