let R be gcdDomain; :: thesis: for Amp, Amp9 being AmpleSet of R
for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9
let Amp, Amp9 be AmpleSet of R; :: thesis: for x, y being Element of R st x,y are_canonical_wrt Amp holds
x,y are_canonical_wrt Amp9
let x, y be Element of R; :: thesis: ( x,y are_canonical_wrt Amp implies x,y are_canonical_wrt Amp9 )
(1. R) * x = x ;
then A1: 1. R divides x ;
(1. R) * y = y ;
then A2: 1. R divides y ;
assume x,y are_canonical_wrt Amp ; :: thesis: x,y are_canonical_wrt Amp9
then gcd (x,y,Amp) = 1. R ;
then A3: for z being Element of R st z divides x & z divides y holds
z divides 1. R by Def12;
1. R in Amp9 by Def8;
then gcd (x,y,Amp9) = 1. R by A3, A1, A2, Def12;
hence x,y are_canonical_wrt Amp9 ; :: thesis: verum