set T = { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ;
for m being Element of NAT ex n being Element of NAT st
( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )

proof

let m be Element of NAT ; :: thesis: ex n being Element of NAT st
( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )
set m' = m + 1;
consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified & 4 * (m + 1) in X ) by Th14;
set n = 4 * (m + 1);
take 4 * (m + 1) ; :: thesis: ( 4 * (m + 1) >= m & 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )
(4 * (m + 1)) + 0 = (1 * (m + 1)) + (3 * (m + 1)) ;
then A2: 4 * (m + 1) >= (m + 1) + 0 by XREAL_1:8;
m + 1 >= m by NAT_1:11;
hence 4 * (m + 1) >= m by A2, XXREAL_0:2; :: thesis: 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) }
( 4 * (m + 1) in X & X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ) by A1;
hence 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } by TARSKI:def 4; :: thesis: verum

end;

then A3: not union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is finite by Th9;

now

let X be set ; :: thesis: ( X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } implies X is finite )
assume X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ; :: thesis: X is finite
then ex X' being Pythagorean_triple st
( X = X' & not X' is degenerate & X' is simplified ) ;
hence X is finite ; :: thesis: verum

end;

hence not { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is finite by A3, FINSET_1:25; :: thesis: verum