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 )
A1: 1. R in Amp by Def8;
0. R is Element of Amp by Th24;
hence ( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R ) by A1, Def9; :: thesis: verum