:: deftheorem defines simplified PYTHTRIP:def 7 :
for X being Pythagorean_triple holds
( X is simplified iff for k being Nat st ( for n being Nat st n in X holds
k divides n ) holds
k = 1 );