theorem Th9: :: WSIERP_1:9

for k being Integer holds 1,k are_coprime