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 Th31;
hence gcd (0. R),(0. R),Amp = 0. R by Th25; :: thesis: verum