theorem id1: :: RING_2:5

for R being Ring
for C being ascending Chain of (Ideals R) holds union { (C . i) where i is Nat : verum } is Ideal of R