let m, n be positive Nat; :: thesis: for s being natural Number st Polygon (s,m) = Polygon (s,n) & s >= 2 holds
m = n
let s be natural Number ; :: thesis: ( Polygon (s,m) = Polygon (s,n) & s >= 2 implies m = n )
assume Polygon (s,m) = Polygon (s,n) ; :: thesis: ( not s >= 2 or m = n )
then ((((m ^2) * (s - 2)) - (m * (s - 4))) - ((n ^2) * (s - 2))) + (n * (s - 4)) = 0 ;
then (m - n) * (((s - 2) * ((m + n) - 1)) + 2) = 0 ;
then A1: ( m - n = 0 or ((s - 2) * ((m + n) - 1)) + 2 = 0 ) ;
assume A2: s >= 2 ; :: thesis: m = n

now :: thesis: not ((s - 2) * ((m + n) - 1)) + 2 = 0

assume A3: ((s - 2) * ((m + n) - 1)) + 2 = 0 ; :: thesis: contradiction
s - 2 >= 2 - 2 by A2, XREAL_1:6;
hence contradiction by A3; :: thesis: verum

end;

hence m = n by A1; :: thesis: verum