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, Def3;
then consider D being Element of R such that
A2: (0. R) * D = A by Def1;
thus 0. R is Element of Amp by A2, VECTSP_1:39; :: thesis: verum