let R be commutative domRing-like Ring; :: thesis: for Amp being AmpleSet of R holds
( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R )
let Amp be AmpleSet of R; :: thesis: ( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R )
( 1. R in Amp & 0. R is Element of Amp ) by Def8, Th24;
hence ( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R ) by Def9; :: thesis: verum