let R be gcdDomain; :: thesis: for Amp being AmpleSet of R
for x, y being Element of R st x,y are_co-prime holds
gcd (x,y,Amp) = 1. R
let Amp be AmpleSet of R; :: thesis: for x, y being Element of R st x,y are_co-prime holds
gcd (x,y,Amp) = 1. R
let x, y be Element of R; :: thesis: ( x,y are_co-prime implies gcd (x,y,Amp) = 1. R )
assume x,y are_co-prime ; :: thesis: gcd (x,y,Amp) = 1. R
then consider Amp9 being AmpleSet of R such that
A1: gcd (x,y,Amp9) = 1. R by Def14;
x,y are_canonical_wrt Amp9 by A1, Def13;
then x,y are_canonical_wrt Amp by Th43;
hence gcd (x,y,Amp) = 1. R by Def13; :: thesis: verum