let R be non empty doubleLoopStr ; :: thesis: ( ( 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 ; :: thesis: 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 ; :: thesis: contradiction
defpred S₁[ 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 & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in NAT implies ex u being object st
( u in the carrier of R & S₁[e,u] ) )
assume e in NAT ; :: thesis: ex u being object st
( u in the carrier of R & S₁[e,u] )
then reconsider n = e as Element of NAT ;

per cases ( n = 0 or n > 0 ) ;

suppose A5: n = 0 ; :: thesis: ex u being object st
( u in the carrier of R & S₁[e,u] )

F . 0 is Ideal of R by A2;
then consider u being object such that
A6: u in F . 0 by XBOOLE_0:def 1;
take u ; :: thesis: ( u in the carrier of R & S₁[e,u] )
thus u in the carrier of R by A6; :: thesis: S₁[e,u]
take n ; :: thesis: ( n = e & ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus n = e ; :: thesis: ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) ) by A5, A6; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex u being object st
( u in the carrier of R & S₁[e,u] )

then consider k being Nat such that
A7: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
n > k by A7, NAT_1:13;
then not F . n c= F . k by A3, XBOOLE_1:60;
then not (F . n) \ (F . k) is empty by XBOOLE_1:37;
then consider u being object such that
A8: u in (F . n) \ (F . k) ;
take u ; :: thesis: ( u in the carrier of R & S₁[e,u] )
thus u in the carrier of R by A8; :: thesis: S₁[e,u]
take n ; :: thesis: ( n = e & ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus n = e ; :: thesis: ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) )
thus ( ( n = 0 implies u in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & u in (F . n) \ (F . k) ) ) ) by A7, A8; :: thesis: verum

end;

end;

end;

consider f being sequence of the carrier of R such that
A9: for e being object st e in NAT holds
S₁[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 S₂[ Nat] means rng (f | (Segm ($1 + 1))) c= F . $1;
A12: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A13: rng (f | (Segm (k + 1))) c= F . k ; :: thesis: S₂[k + 1]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (Segm ((k + 1) + 1))) or y in F . (k + 1) )
assume y in rng (f | (Segm ((k + 1) + 1))) ; :: thesis: y in F . (k + 1)
then consider x being object such that
A14: x in dom (f | (Segm ((k + 1) + 1))) and
A15: y = (f | (Segm ((k + 1) + 1))) . x by FUNCT_1:def 3;
A16: x in dom f by A14, RELAT_1:57;
reconsider nx = x as Element of NAT by A14;
x in Segm ((k + 1) + 1) by A14, RELAT_1:57;
then nx < (k + 1) + 1 by NAT_1:44;
then A17: nx <= k + 1 by NAT_1:13;

per cases ( nx < k + 1 or nx = k + 1 ) by A17, XXREAL_0:1;

suppose nx < k + 1 ; :: thesis: y in F . (k + 1)

then A18: nx in Segm (k + 1) by NAT_1:44;
k < k + 1 by NAT_1:13;
then F . k c< F . (k + 1) by A3;
then A19: F . k c= F . (k + 1) ;
y = f . nx by A14, A15, FUNCT_1:47;
then y in rng (f | (Segm (k + 1))) by A16, A18, FUNCT_1:50;
then y in F . k by A13;
hence y in F . (k + 1) by A19; :: thesis: verum

end;

suppose A20: nx = k + 1 ; :: thesis: y in F . (k + 1)

( y = f . nx & ex n being Element of NAT st
( n = nx & ( n = 0 implies f . nx in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . nx in (F . n) \ (F . k) ) ) ) ) by A9, A14, A15, FUNCT_1:47;
hence y in F . (k + 1) by A20, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

F . m is Ideal of R by A2;
then A21: F . m = (F . m) -Ideal by Th44;
A22: S₂[ 0 ]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f | (Segm (0 + 1))) or y in F . 0 )
assume y in rng (f | (Segm (0 + 1))) ; :: thesis: y in F . 0
then consider x being object such that
A23: x in dom (f | (Segm 1)) and
A24: y = (f | (Segm 1)) . x by FUNCT_1:def 3;
( x in Segm 1 & ex n being Element of NAT st
( n = x & ( n = 0 implies f . x in F . 0 ) & ( n > 0 implies ex k being Element of NAT st
( n = k + 1 & f . x in (F . n) \ (F . k) ) ) ) ) by A9, A23, RELAT_1:57;
hence y in F . 0 by A24, CARD_1:49, FUNCT_1:49, TARSKI:def 1; :: thesis: verum

end;

for m being Nat holds S₂[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; :: thesis: verum