thus [#] R is left-ideal :: thesis: [#] R is right-ideal
proof
let x, y be Element of R; :: according to IDEAL_1:def 2 :: thesis: ( not y in [#] R or x * y in [#] R )
thus ( not y in [#] R or x * y in [#] R ) ; :: thesis: verum
end;
let x, y be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not y in [#] R or y * x in [#] R )
thus ( not y in [#] R or y * x in [#] R ) ; :: thesis: verum