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