theorem :: IDEAL_1:99

for R being non empty doubleLoopStr st ( 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 ) ) ) holds
R is Noetherian