let F be Chain of (Ideals R); ( F is ascending implies F is stagnating )
set G = { (F . i) where i is Nat : verum } ;
assume AS:
F is ascending
; F is stagnating
then reconsider I = union { (F . i) where i is Nat : verum } as Ideal of R by id1;
I is principal
by IDEAL_1:def 28;
then consider a being Element of R such that
H0:
I = {a} -Ideal
;
a in I
by H0, IDEAL_1:66;
then consider x1 being set such that
H1:
( a 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 Fi being Ideal of R such that
H3:
Fi = F . i
;
Fi c= I
by H1, H2, H3, TARSKI:def 4;
then B4:
Fi = I
by H0, H1, H2, H3, id2;
now for j being Nat st j >= i holds
F . j = F . ilet j be
Nat;
( j >= i implies F . j = F . i )
F . j in Ideals R
;
then consider Fj being
Ideal of
R such that H:
Fj = F . j
;
B5:
F . j in { (F . i) where i is Nat : verum }
;
assume X:
j >= i
;
F . j = F . i
Fj c= I
by H, B5, TARSKI:def 4;
hence
F . j = F . i
by B4, H, H3, H0, id2, H1, H2, ch1, AS, X;
verum end;
hence
F is stagnating
; verum