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