let n be 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 n is odd ) ;

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

then consider m being Nat such that
A2: n = 2 * m ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
set c = 1 * ((m ^2) + (1 ^2));
set b = 1 * ((2 * 1) * m);
2 * m > 2 * 1 by A1, A2;
then A3: m > 1 by XREAL_1:64;
then m ^2 > 1 ^2 by SQUARE_1:16;
then (m ^2) - (1 ^2) > 0 by XREAL_1:50;
then reconsider a = 1 * ((m ^2) - (1 ^2)) as Element of NAT by INT_1:3;
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:16;
hence not 0 in X by A1, A2, ENUMSET1:def 1; :: according to ORDINAL1:def 16 :: thesis: n in X
thus n in X by A2, ENUMSET1:def 1; :: thesis: verum

end;

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

then consider i being Integer such that
A4: n = (2 * i) + 1 by ABIAN:1;
A5: 2 * i >= 2 * 1 by A1, A4, INT_1:7;
then i >= 1 by XREAL_1:68;
then reconsider m = i as Element of NAT by INT_1:3;
reconsider a = 1 * (((m + 1) ^2) - (m ^2)) as Element of NAT by A4, ORDINAL1:def 12;
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 )
( a = (2 * m) + 1 & 1 * (((m + 1) ^2) + (m ^2)) = (((m ^2) + (2 * m)) + (m ^2)) + 1 ) ;
hence not 0 in X by A5, ENUMSET1:def 1; :: according to ORDINAL1:def 16 :: thesis: n in X
thus n in X by A4, ENUMSET1:def 1; :: thesis: verum

end;

end;