:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :
for X being Pythagorean_triple holds
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_coprime ) );