:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :
for b₁ being Subset of NAT holds
( b₁ is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b₁ = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) );