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