let x, y be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not x in [#] R or not y in [#] R or x + y in [#] R )
thus ( not x in [#] R or not y in [#] R or x + y in [#] R ) ; :: thesis: verum