theorem :: PYTHTRIP:13

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