( a gcd b divides a & a gcd b divides b ) by INT_2:def 2;
hence (a + b) / (a gcd b) is integer by Th1, WSIERP_1:4; :: thesis: verum