let R be non empty doubleLoopStr ; :: thesis: for I being non empty add-closed Subset of R holds I is Preserv of the addF of R
let I be non empty add-closed Subset of R; :: thesis: I is Preserv of the addF of R
I is the addF of R -binopclosed

proof

let x be set ; :: according to REALSET1:def 1 :: thesis: ( not x in [:I,I:] or the addF of R . x in I )
assume x in [:I,I:] ; :: thesis: the addF of R . x in I
then consider y, z being object such that
A1: ( y in I & z in I ) and
A2: x = [y,z] by ZFMISC_1:def 2;
reconsider y = y, z = z as Element of I by A1;
the addF of R . x = y + z by A2;
hence the addF of R . x in I by IDEAL_1:def 1; :: thesis: verum

end;

hence I is Preserv of the addF of R ; :: thesis: verum