theorem Th1: :: PYTHTRIP:1

for m, n being Nat st m * n is square & m,n are_coprime holds
( m is square & n is square )