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