let X be Pythagorean_triple ; :: thesis: X is finite

ex a, b, c being Element of NAT st

( (a ^2) + (b ^2) = c ^2 & X = {a,b,c} ) by Def4;

hence X is finite ; :: thesis: verum

ex a, b, c being Element of NAT st

( (a ^2) + (b ^2) = c ^2 & X = {a,b,c} ) by Def4;

hence X is finite ; :: thesis: verum