let R be non empty doubleLoopStr ; ( ( for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal ) implies for F being sequence of (bool the carrier of R) holds
( ex i being Nat st F . i is not Ideal of R or ex j, k being Nat st
( j < k & not F . j c< F . k ) ) )
assume A1:
for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal
; for F being sequence of (bool the carrier of R) holds
( ex i being Nat st F . i is not Ideal of R or ex j, k being Nat st
( j < k & not F . j c< F . k ) )
given F being sequence of (bool the carrier of R) such that A2:
for i being Nat holds F . i is Ideal of R
and
A3:
for j, k being Nat st j < k holds
F . j c< F . k
; contradiction
defpred S1[ object , object ] means ex n being Element of NAT st
( n = $1 & ( n = 0 implies $2 in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & $2 in (F . n) \ (F . k) ) ) );
A4:
for e being object st e in NAT holds
ex u being object st
( u in the carrier of R & S1[e,u] )
consider f being sequence of the carrier of R such that
A9:
for e being object st e in NAT holds
S1[e,f . e]
from FUNCT_2:sch 1(A4);
consider m being Element of NAT such that
A10:
f . (m + 1) in (rng (f | (m + 1))) -Ideal
by A1;
reconsider m1 = m + 1 as non zero Nat ;
A11:
ex n being Element of NAT st
( n = m + 1 & ( n = 0 implies f . (m + 1) in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . (m + 1) in (F . n) \ (F . k) ) ) )
by A9;
defpred S2[ Nat] means rng (f | (Segm ($1 + 1))) c= F . $1;
A12:
for k being Nat st S2[k] holds
S2[k + 1]
F . m is Ideal of R
by A2;
then A21:
F . m = (F . m) -Ideal
by Th44;
A22:
S2[ 0 ]
for m being Nat holds S2[m]
from NAT_1:sch 2(A22, A12);
then
(rng (f | (Segm m1))) -Ideal c= F . m
by A21, Th57;
hence
contradiction
by A10, A11, XBOOLE_0:def 5; verum