for n being Element of NAT st n > 0 holds
ex X being Pythagorean_triple st
( not X is degenerate & X is simplified & 4 * n in X )