:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :
for b₁ being Subset of NAT holds
( b₁ is Pythagorean_triple iff ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b₁ = {a,b,c} ) );