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 in Amp by Def12;
A2: ( gcd A,B,Amp divides B & gcd A,B,Amp divides A ) by Def12;
for z being Element of R st z divides B & z divides A holds
z divides gcd A,B,Amp by Def12;
hence gcd A,B,Amp = gcd B,A,Amp by A1, A2, Def12; :: thesis: verum