theorem :: FVALUAT1:67

for R being non empty doubleLoopStr
for I being non empty add-closed Subset of R holds I is Preserv of the addF of R