let R be gcdDomain; :: thesis: for Amp being AmpleSet of R holds gcd ((0. R),(0. R),Amp) = 0. R
let Amp be AmpleSet of R; :: thesis: gcd ((0. R),(0. R),Amp) = 0. R
gcd ((0. R),(0. R),Amp) = NF ((0. R),Amp) by Th30;
hence gcd ((0. R),(0. R),Amp) = 0. R by Th25; :: thesis: verum