let a be Element of R; :: thesis: a is_associated_to a
thus ( a divides a & a divides a ) ; :: according to GCD_1:def 3 :: thesis: verum