let R be commutative domRing-like Ring; :: thesis: for Amp being AmpleSet of R holds 0. R is Element of Amp
let Amp be AmpleSet of R; :: thesis: 0. R is Element of Amp
consider A being Element of Amp such that
A1: A is_associated_to 0. R by Th22;
0. R divides A by A1;
then ex D being Element of R st (0. R) * D = A ;
hence 0. R is Element of Amp ; :: thesis: verum