let R be Ring; :: thesis: for C being ascending Chain of (Ideals R) holds union { (C . i) where i is Nat : verum } is Ideal of R
let F be ascending Chain of (Ideals R); :: thesis: union { (F . i) where i is Nat : verum } is Ideal of R
set G = { (F . i) where i is Nat : verum } ;
set T = union { (F . i) where i is Nat : verum } ;
M: F . 0 in { (F . i) where i is Nat : verum } ;
F . 0 in Ideals R ;
then consider I being Ideal of R such that
H: I = F . 0 ;
set x = the Element of I;
L: ex Y being set st
( the Element of I in Y & Y in { (F . i) where i is Nat : verum } ) by M, H;

now :: thesis: for x being object st x in union { (F . i) where i is Nat : verum } holds
x in the carrier of R

let x be object ; :: thesis: ( x in union { (F . i) where i is Nat : verum } implies x in the carrier of R )
assume x in union { (F . i) where i is Nat : verum } ; :: thesis: x in the carrier of R
then consider x1 being set such that
H1: ( x in x1 & x1 in { (F . i) where i is Nat : verum } ) by TARSKI:def 4;
consider i being Nat such that
H2: x1 = F . i by H1;
F . i in Ideals R ;
hence x in the carrier of R by H1, H2; :: thesis: verum

end;

then union { (F . i) where i is Nat : verum } c= the carrier of R ;
then reconsider T = union { (F . i) where i is Nat : verum } as non empty Subset of R by L, TARSKI:def 4;

now :: thesis: for x, y being Element of R st x in T & y in T holds
x + y in T

let x, y be Element of R; :: thesis: ( x in T & y in T implies x + y in T )
assume H0: ( x in T & y in T ) ; :: thesis: x + y in T
then consider x1 being set such that
H1: ( x in x1 & x1 in { (F . i) where i is Nat : verum } ) by TARSKI:def 4;
consider i being Nat such that
H2: x1 = F . i by H1;
F . i in Ideals R ;
then consider Ix being Ideal of R such that
H5: Ix = F . i ;
consider y1 being set such that
H3: ( y in y1 & y1 in { (F . i) where i is Nat : verum } ) by H0, TARSKI:def 4;
consider j being Nat such that
H4: y1 = F . j by H3;
F . j in Ideals R ;
then consider Iy being Ideal of R such that
H6: Iy = F . j ;

now :: thesis: ex Y being set st
( x + y in Y & Y in { (F . i) where i is Nat : verum } )

per cases ( i <= j or j <= i ) ;

suppose i <= j ; :: thesis: ex Y being set st
( x + y in Y & Y in { (F . i) where i is Nat : verum } )

then x in Iy by H6, H2, H1, ch1;
hence ex Y being set st
( x + y in Y & Y in { (F . i) where i is Nat : verum } ) by H3, H4, H6, IDEAL_1:def 1; :: thesis: verum

end;

suppose j <= i ; :: thesis: ex Y being set st
( x + y in Y & Y in { (F . i) where i is Nat : verum } )

then y in Ix by H5, H3, H4, ch1;
hence ex Y being set st
( x + y in Y & Y in { (F . i) where i is Nat : verum } ) by H2, H1, H5, IDEAL_1:def 1; :: thesis: verum

end;

end;

end;

hence x + y in T by TARSKI:def 4; :: thesis: verum

end;

then A: T is add-closed ;

now :: thesis: for p, x being Element of R st x in T holds
p * x in T

let p, x be Element of R; :: thesis: ( x in T implies p * x in T )
assume x in T ; :: thesis: p * x in T
then consider x1 being set such that
H1: ( x in x1 & x1 in { (F . i) where i is Nat : verum } ) by TARSKI:def 4;
consider i being Nat such that
H2: x1 = F . i by H1;
F . i in Ideals R ;
then consider Ix being Ideal of R such that
H5: Ix = F . i ;
p * x in Ix by H1, H2, H5, IDEAL_1:def 2;
hence p * x in T by H5, H2, H1, TARSKI:def 4; :: thesis: verum

end;

then B: T is left-ideal ;

now :: thesis: for p, x being Element of R st x in T holds
x * p in T

let p, x be Element of R; :: thesis: ( x in T implies x * p in T )
assume x in T ; :: thesis: x * p in T
then consider x1 being set such that
H1: ( x in x1 & x1 in { (F . i) where i is Nat : verum } ) by TARSKI:def 4;
consider i being Nat such that
H2: x1 = F . i by H1;
F . i in Ideals R ;
then consider Ix being Ideal of R such that
H5: Ix = F . i ;
x * p in Ix by H1, H2, H5, IDEAL_1:def 3;
hence x * p in T by H1, H2, H5, TARSKI:def 4; :: thesis: verum

end;

then T is right-ideal ;
hence union { (F . i) where i is Nat : verum } is Ideal of R by A, B; :: thesis: verum