let x, y be Element of R; :: thesis: ( (R,x,y) implies (R,y,x) )
given Amp being AmpleSet of R such that A1: gcd (x,y,Amp) = 1. R ; :: according to GCD_1:def 14 :: thesis: (R,y,x)
gcd (y,x,Amp) = 1. R by A1, Th29;
hence (R,y,x) ; :: thesis: verum