let R be non empty doubleLoopStr ; :: thesis: ( ( for F being sequence of (bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) ) ) implies R is Noetherian )
assume that
A1: for F being sequence of (bool the carrier of R) holds
( ex i being Element of NAT st F . i is not Ideal of R or ex j, k being Element of NAT st
( j < k & not F . j c< F . k ) ) and
A2: not R is Noetherian ; :: thesis: contradiction
consider I being Ideal of R such that
A3: not I is finitely_generated by A2;
set D = { S where S is Subset of R : S is non empty finite Subset of I } ;
consider e being object such that
A4: e in I by XBOOLE_0:def 1;
reconsider e = e as Element of R by A4;
{e} c= I by A4, ZFMISC_1:31;
then A5: {e} in { S where S is Subset of R : S is non empty finite Subset of I } ;
{ S where S is Subset of R : S is non empty finite Subset of I } c= bool the carrier of R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Subset of R : S is non empty finite Subset of I } or x in bool the carrier of R )
assume x in { S where S is Subset of R : S is non empty finite Subset of I } ; :: thesis: x in bool the carrier of R
then ex s being Subset of R st
( x = s & s is non empty finite Subset of I ) ;
hence x in bool the carrier of R ; :: thesis: verum
end;
then reconsider D = { S where S is Subset of R : S is non empty finite Subset of I } as non empty Subset-Family of R by A5;
reconsider e9 = {e} as Element of D by A5;
defpred S1[ set , Element of D, set ] means ex r being Element of R st
( r in I \ ($2 -Ideal) & $3 = $2 \/ {r} );
A6: for n being Nat
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of D ex y being Element of D st S1[n,x,y]
let x be Element of D; :: thesis: ex y being Element of D st S1[n,x,y]
x in D ;
then consider x9 being Subset of R such that
A7: x9 = x and
A8: x9 is non empty finite Subset of I ;
reconsider x19 = x9 as non empty finite Subset of I by A8;
x9 -Ideal c= I -Ideal by A8, Th57;
then x9 -Ideal c= I by Th44;
then not I c= x9 -Ideal by A3, A8, XBOOLE_0:def 10;
then consider r being object such that
A9: r in I and
A10: not r in x9 -Ideal ;
set y = x19 \/ {r};
A11: x19 \/ {r} c= I
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in x19 \/ {r} or x in I )
assume x in x19 \/ {r} ; :: thesis: x in I
then ( x in x19 or x in {r} ) by XBOOLE_0:def 3;
hence x in I by A9, TARSKI:def 1; :: thesis: verum
end;
then x19 \/ {r} is Subset of R by XBOOLE_1:1;
then A12: x19 \/ {r} in D by A11;
reconsider r = r as Element of R by A9;
reconsider y = x19 \/ {r} as Element of D by A12;
take y ; :: thesis: S1[n,x,y]
take r ; :: thesis: ( r in I \ (x -Ideal) & y = x \/ {r} )
thus ( r in I \ (x -Ideal) & y = x \/ {r} ) by A7, A9, A10, XBOOLE_0:def 5; :: thesis: verum
end;
consider f being sequence of D such that
A13: ( f . 0 = e9 & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A6);
 defpred S2[ Nat, Subset of R] means ex c being Subset of R st
( c = f . $1 & $2 = c -Ideal );
A14: for x being Element of NAT ex y being Subset of R st S2[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Subset of R st S2[x,y]
f . x in D ;
then consider c being Subset of R such that
A15: c = f . x and
c is non empty finite Subset of I ;
reconsider y = c -Ideal as Subset of R ;
take y ; :: thesis: S2[x,y]
take c ; :: thesis: ( c = f . x & y = c -Ideal )
thus ( c = f . x & y = c -Ideal ) by A15; :: thesis: verum
end;
consider F being sequence of (bool the carrier of R) such that
A16: for x being Element of NAT holds S2[x,F . x] from FUNCT_2:sch 3(A14);
 A17: for x being Nat holds S2[x,F . x]
proof
let x be Nat; :: thesis: S2[x,F . x]
x in NAT by ORDINAL1:def 12;
hence S2[x,F . x] by A16; :: thesis: verum
end;
A18: for j, k being Element of NAT st j < k holds
F . j c< F . k
proof
let j, k be Element of NAT ; :: thesis: ( j < k implies F . j c< F . k )
defpred S3[ Nat] means F . j c< F . ((j + 1) + $1);
assume j < k ; :: thesis: F . j c< F . k
then j + 1 <= k by NAT_1:13;
then consider i being Nat such that
A19: k = (j + 1) + i by NAT_1:10;
A20: for i being Nat holds F . i c< F . (i + 1)
proof
let i be Nat; :: thesis: F . i c< F . (i + 1)
consider c being Subset of R such that
A21: c = f . i and
A22: F . i = c -Ideal by A17;
consider c1 being Subset of R such that
A23: c1 = f . (i + 1) and
A24: F . (i + 1) = c1 -Ideal by A17;
A25: c1 c= c1 -Ideal by Def14;
consider r being Element of R such that
A26: r in I \ (c -Ideal) and
A27: c1 = c \/ {r} by A13, A21, A23;
c in D by A21;
then ex c9 being Subset of R st
( c9 = c & c9 is non empty finite Subset of I ) ;
hence F . i c= F . (i + 1) by A22, A24, A27, Th57, XBOOLE_1:7; :: according to XBOOLE_0:def 8 :: thesis: not F . i = F . (i + 1)
r in {r} by TARSKI:def 1;
then r in c1 by A27, XBOOLE_0:def 3;
hence not F . i = F . (i + 1) by A22, A24, A26, A25, XBOOLE_0:def 5; :: thesis: verum
end;
A28: for i being Nat st S3[i] holds
S3[i + 1]
proof
let i be Nat; :: thesis: ( S3[i] implies S3[i + 1] )
assume that
A29: F . j c= F . ((j + 1) + i) and
F . j <> F . ((j + 1) + i) ; :: according to XBOOLE_0:def 8 :: thesis: S3[i + 1]
A30: F . ((j + 1) + i) c< F . (((j + 1) + i) + 1) by A20;
then F . ((j + 1) + i) c= F . (((j + 1) + i) + 1) ;
hence F . j c= F . ((j + 1) + (i + 1)) by A29; :: according to XBOOLE_0:def 8 :: thesis: not F . j = F . ((j + 1) + (i + 1))
thus not F . j = F . ((j + 1) + (i + 1)) by A29, A30, XBOOLE_0:def 8; :: thesis: verum
end;
A31: S3[ 0 ] by A20;
A32: for i being Nat holds S3[i] from NAT_1:sch 2(A31, A28);
 thus F . j c< F . k by A32, A19; :: thesis: verum
end;
for i being Element of NAT holds F . i is Ideal of R
proof
let i be Element of NAT ; :: thesis: F . i is Ideal of R
ex c being Subset of R st
( c = f . i & F . i = c -Ideal ) by A17;
hence F . i is Ideal of R ; :: thesis: verum
end;
hence contradiction by A1, A18; :: thesis: verum