let A be non degenerated comRing; :: thesis: for F being non empty Subset of (Ideals A) holds union F is non empty Subset of A
let F be non empty Subset of (Ideals A); :: thesis: union F is non empty Subset of A
consider I being object such that
A1: I in F by XBOOLE_0:def 1;
I in Ideals A by A1;
then I in { J where J is Ideal of A : verum } by RING_2:def 3;
then consider I1 being Ideal of A such that
A2: I = I1 ;
0. A in I1 by IDEAL_1:2;
then A3: 0. A in union F by A1, A2, TARSKI:def 4;
for I being set st I in F holds
I c= [#] A

proof

let I be set ; :: thesis: ( I in F implies I c= [#] A )
assume I in F ; :: thesis: I c= [#] A
then I in Ideals A ;
then I in { J where J is Ideal of A : verum } by RING_2:def 3;
then consider I1 being Ideal of A such that
A5: I = I1 ;
thus I c= [#] A by A5; :: thesis: verum

end;

hence union F is non empty Subset of A by A3, XBOOLE_0:def 1, ZFMISC_1:76; :: thesis: verum