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

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

hence
I is Preserv of the addF of R
; :: thesis: verum
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;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