:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
for R being non empty well-unital associative multLoopStr
for b₂ being non empty Subset of R holds
( b₂ is AmpleSet of R iff ( b₂ is Am of R & 1. R in b₂ ) );