for a, b, c, m, n being Element of NAT st a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) holds
(a ^2) + (b ^2) = c ^2 ;