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 Amp' being AmpleSet of R such that
A1: gcd x,y,Amp' = 1. R by Def14;
x,y are_canonical_wrt Amp' by A1, Def13;
then x,y are_canonical_wrt Amp by Th43;
hence gcd x,y,Amp = 1. R by Def13; :: thesis: verum