let a, b be Integer; :: thesis: a,b are_congruent_mod a gcd b
( a gcd b divides a & a gcd b divides b ) by INT_2:def 2;
hence a,b are_congruent_mod a gcd b by INT_5:1; :: thesis: verum