let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for a, b being Element of R holds gcd (a,b,Amp) = gcd (b,a,Amp)
let Amp be AmpleSet of R; :: thesis: for a, b being Element of R holds gcd (a,b,Amp) = gcd (b,a,Amp)
let A, B be Element of R; :: thesis: gcd (A,B,Amp) = gcd (B,A,Amp)
set D = gcd (A,B,Amp);
A1: ( gcd (A,B,Amp) divides A & ( for z being Element of R st z divides B & z divides A holds
z divides gcd (A,B,Amp) ) ) by Def12;
( gcd (A,B,Amp) in Amp & gcd (A,B,Amp) divides B ) by Def12;
hence gcd (A,B,Amp) = gcd (B,A,Amp) by A1, Def12; :: thesis: verum