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