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