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