:: deftheorem Def6 defines degenerate PYTHTRIP:def 6 :
for X being Pythagorean_triple holds
( X is degenerate iff 0 in X );