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