let n be Element of NAT ; :: thesis: ( n > 2 implies ex X being Pythagorean_triple st
( not X is degenerate & n in X ) )
assume A1: n > 2 ; :: thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )

then consider m being Element of NAT such that
A2: n = 2 * m by ABIAN:def 2;
2 * m > 2 * 1 by A1, A2;
then A3: m > 1 by XREAL_1:66;
then m ^2 > 1 ^2 by SQUARE_1:78;
then (m ^2 ) - (1 ^2 ) > 0 by XREAL_1:52;
then reconsider a = 1 * ((m ^2 ) - (1 ^2 )) as Element of NAT by INT_1:16;
set b = 1 * ((2 * 1) * m);
set c = 1 * ((m ^2 ) + (1 ^2 ));
reconsider X = {a,(1 * ((2 * 1) * m)),(1 * ((m ^2 ) + (1 ^2 )))} as Pythagorean_triple by A3, Def5;
take X ; :: thesis: ( not X is degenerate & n in X )
a <> 0 by A3, SQUARE_1:78;
hence not 0 in X by A1, A2, ENUMSET1:def 1; :: according to PYTHTRIP:def 6 :: thesis: n in X
thus n in X by A2, ENUMSET1:def 1; :: thesis: verum

end;

suppose not n is even ; :: thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )

then consider i being Integer such that
A5: n = (2 * i) + 1 by ABIAN:1;
A6: 2 * i >= 2 * 1 by A1, A5, INT_1:20;
then i >= 1 by XREAL_1:70;
then reconsider m = i as Element of NAT by INT_1:16;
reconsider a = 1 * (((m + 1) ^2 ) - (m ^2 )) as Element of NAT by A5;
set b = 1 * ((2 * m) * (m + 1));
set c = 1 * (((m + 1) ^2 ) + (m ^2 ));
m <= m + 1 by NAT_1:11;
then reconsider X = {a,(1 * ((2 * m) * (m + 1))),(1 * (((m + 1) ^2 ) + (m ^2 )))} as Pythagorean_triple by Def5;
take X ; :: thesis: ( not X is degenerate & n in X )
A7: a = (2 * m) + 1 ;
A8: 1 * (((m + 1) ^2 ) + (m ^2 )) = (((m ^2 ) + (2 * m)) + (m ^2 )) + 1 ;
1 * ((2 * m) * (m + 1)) <> 0 by A6, XCMPLX_1:6;
hence not 0 in X by A7, A8, ENUMSET1:def 1; :: according to PYTHTRIP:def 6 :: thesis: n in X
thus n in X by A5, ENUMSET1:def 1; :: thesis: verum

end;

end;