theorem :: PYTHTRIP:13

for n being Element of NAT st n > 2 holds
ex X being Pythagorean_triple st
( not X is degenerate & n in X )