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 m9 = m + 1;
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 ) } )
consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified ) and
A2: 4 * (m + 1) in X by Th14;
(4 * (m + 1)) + 0 = (1 * (m + 1)) + (3 * (m + 1)) ;
then A3: 4 * (m + 1) >= (m + 1) + 0 by XREAL_1:6;
m + 1 >= m by NAT_1:11;
hence 4 * (m + 1) >= m by A3, XXREAL_0:2; :: thesis: 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) }
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 A2, TARSKI:def 4; :: thesis: verum

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 X9 being Pythagorean_triple st
( X = X9 & not X9 is degenerate & X9 is simplified ) ;
hence X is finite ; :: thesis: verum