let R be non empty connected Poset; :: thesis:
assume A1: R is well_founded ; :: thesis:
set IR = the InternalRel of R;
set CR = the carrier of R;
set FIR = FinOrd R;
set FCR = Fin the carrier of R;
assume not FinPoset R is well_founded ; :: thesis:
then consider A being sequence of (FinPoset R) such that
A2: A is descending by WELLFND1:15;
set zz = { z where z is sequence of (FinPoset R) : z is descending } ;
A in { z where z is sequence of (FinPoset R) : z is descending } by A2;
then reconsider zz = { z where z is sequence of (FinPoset R) : z is descending } as non empty set ;
set Z = [:the carrier of R,zz:];
defpred S₁[ Nat, set , set ] means ex Sn2 being sequence of (FinPoset R) ex Smax being Function of NAT ,the carrier of R ex an being Element of ex ix being Nat ex bnt, bn being sequence of (FinPoset R) st
( Sn2 = $2 `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & an = MinElement (rng Smax),R & ix = Smax mindex an & bnt = Sn2 ^\ ix & ( for i being Nat holds bn . i = (bnt . i) \ {an} ) & ( for i being Nat st ix <= i holds
Smax . i = an ) & $3 = [an,bn] );
A3: for n being Element of NAT
for Sn being Element of [:the carrier of R,zz:] ex Sn1 being Element of [:the carrier of R,zz:] st S₁[n,Sn,Sn1]

let n be Element of NAT ; :: thesis:
let Sn be Element of [:the carrier of R,zz:]; :: thesis:
set Sn2 = Sn `2 ;
Sn `2 in zz ;
then A4: ex z being sequence of (FinPoset R) st
( z = Sn `2 & z is descending ) ;
then reconsider Sn2 = Sn `2 as sequence of (FinPoset R) ;

A5: now

let i be Nat; :: thesis:
assume A6: Sn2 . i = {} ; :: thesis:
A7: Sn2 . (i + 1) <> Sn2 . i by A4, WELLFND1:def 7;
[(Sn2 . (i + 1)),(Sn2 . i)] in FinOrd R by A4, WELLFND1:def 7;
hence contradiction by A6, A7, Th37; :: thesis:

end;

defpred S₂[ Nat, set ] means ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . $1 & Sn2i <> {} & $2 = PosetMax Sn2i );
A8: for i being Element of NAT ex y being Element of the carrier of R st S₂[i,y]

proof

let i be Element of NAT ; :: thesis:
set Sn2i = Sn2 . i;
reconsider Sn2i = Sn2 . i as Element of Fin the carrier of R ;
set y = PosetMax Sn2i;
take PosetMax Sn2i ; :: thesis:
take Sn2i ; :: thesis:
thus Sn2i = Sn2 . i ; :: thesis:
thus Sn2i <> {} by A5; :: thesis:
thus PosetMax Sn2i = PosetMax Sn2i ; :: thesis:

end;

consider Smax being Function of NAT ,the carrier of R such that
A9: for i being Element of NAT holds S₂[i,Smax . i] from FUNCT_2:sch 3(A8);
set an = MinElement (rng Smax),R;
set ix = Smax mindex (MinElement (rng Smax),R);
set bnt = Sn2 ^\ (Smax mindex (MinElement (rng Smax),R));
defpred S₃[ set , set ] means ex bni being Element of Fin the carrier of R st
( bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . $1) \ {(MinElement (rng Smax),R)} & $2 = bni );

now

let i be Nat; :: thesis:
set bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i) \ {(MinElement (rng Smax),R)};
reconsider k = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i as finite Subset of by FINSUB_1:def 5;
k \ {(MinElement (rng Smax),R)} in Fin the carrier of R by FINSUB_1:def 5;
then reconsider bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i) \ {(MinElement (rng Smax),R)} as Element of Fin the carrier of R ;
set y = bni;
take y = bni; :: thesis:
take bni = bni; :: thesis:
thus bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i) \ {(MinElement (rng Smax),R)} ; :: thesis:
thus y = bni ; :: thesis:

end;

then A10: for i being Element of NAT ex y being Element of Fin the carrier of R st S₃[i,y] ;
defpred S₄[ Nat] means Smax . ((Smax mindex (MinElement (rng Smax),R)) + $1) = MinElement (rng Smax),R;
A11: dom Smax = NAT by FUNCT_2:def 1;
A12: rng Smax c= the carrier of R by RELAT_1:def 19;
then A13: MinElement (rng Smax),R in rng Smax by A1, Def19;
A14: MinElement (rng Smax),R is_minimal_wrt rng Smax,the InternalRel of R by A1, A12, Def19;
A15: S₄[ 0 ] by A11, A13, DICKSON:def 11;

A16: now

let k be Nat; :: thesis:
assume A17: S₄[k] ; :: thesis:
set ixk = (Smax mindex (MinElement (rng Smax),R)) + k;
set ixk1 = (Smax mindex (MinElement (rng Smax),R)) + (k + 1);
set ixk1' = ((Smax mindex (MinElement (rng Smax),R)) + k) + 1;
consider Sn2ixk being Element of Fin the carrier of R such that
A18: Sn2ixk = Sn2 . ((Smax mindex (MinElement (rng Smax),R)) + k) and
Sn2ixk <> {} and
A19: Smax . ((Smax mindex (MinElement (rng Smax),R)) + k) = PosetMax Sn2ixk by A9;
consider Sn2ixk1 being Element of Fin the carrier of R such that
A20: Sn2ixk1 = Sn2 . ((Smax mindex (MinElement (rng Smax),R)) + (k + 1)) and
A21: Sn2ixk1 <> {} and
A22: Smax . ((Smax mindex (MinElement (rng Smax),R)) + (k + 1)) = PosetMax Sn2ixk1 by A9;
reconsider Sn2ixk' = Sn2ixk, Sn2ixk1' = Sn2ixk1 as Element of ;
(Smax mindex (MinElement (rng Smax),R)) + (k + 1) = ((Smax mindex (MinElement (rng Smax),R)) + k) + 1 ;
then [Sn2ixk1',Sn2ixk'] in FinOrd R by A4, A18, A20, WELLFND1:def 7;
then consider x, y being Element of Fin the carrier of R such that
A23: Sn2ixk1 = x and
A24: Sn2ixk = y and
A25: ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ) by Th40;

per cases by A25;

suppose x = {} ; :: thesis:

hence S₄[k + 1] by A21, A23; :: thesis:

end;

suppose A26: ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ; :: thesis:

Smax . ((Smax mindex (MinElement (rng Smax),R)) + (k + 1)) in rng Smax by A11, FUNCT_1:def 5;
hence S₄[k + 1] by A14, A17, A19, A22, A23, A24, A26, WAYBEL_4:def 26; :: thesis:

end;

suppose ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ; :: thesis:

hence S₄[k + 1] by A17, A19, A22, A23, A24; :: thesis:

end;

A27: for k being Nat holds S₄[k] from NAT_1:sch 2(A15, A16);

A28: now

let i be Nat; :: thesis:
assume Smax mindex (MinElement (rng Smax),R) <= i ; :: thesis:
then consider k being Nat such that
A29: i = (Smax mindex (MinElement (rng Smax),R)) + k by NAT_1:10;
reconsider k = k as Nat by ORDINAL1:def 13;
i = (Smax mindex (MinElement (rng Smax),R)) + k by A29;
hence Smax . i = MinElement (rng Smax),R by A27; :: thesis:

end;

A30: now

let i be Nat; :: thesis:
assume A31: Smax mindex (MinElement (rng Smax),R) <= i ; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
consider Sn2i being Element of Fin the carrier of R such that
A32: Sn2i = Sn2 . i and
Sn2i <> {} and
A33: Smax . i0 = PosetMax Sn2i by A9;
take Sn2i = Sn2i; :: thesis:
thus Sn2i = Sn2 . i by A32; :: thesis:
thus PosetMax Sn2i = MinElement (rng Smax),R by A28, A31, A33; :: thesis:

end;

A34: now

let i be Nat; :: thesis:
set bnti = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i;
reconsider bnti = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i as Element of Fin the carrier of R ;
take bnti = bnti; :: thesis:
thus bnti = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i ; :: thesis:
set iix = i + (Smax mindex (MinElement (rng Smax),R));
ex Sn2iix being Element of Fin the carrier of R st
( Sn2iix = Sn2 . (i + (Smax mindex (MinElement (rng Smax),R))) & PosetMax Sn2iix = MinElement (rng Smax),R ) by A30, NAT_1:11;
hence PosetMax bnti = MinElement (rng Smax),R by NAT_1:def 3; :: thesis:

end;

consider bn being Function of NAT , Fin the carrier of R such that
A35: for i being Element of NAT holds S₃[i,bn . i] from FUNCT_2:sch 3(A10);
reconsider bn = bn as sequence of (FinPoset R) ;
set Sn1 = [(MinElement (rng Smax),R),bn];
A36: Sn2 ^\ (Smax mindex (MinElement (rng Smax),R)) is descending by A4, Th41;

now

let i be Nat; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
A37: ex bni being Element of Fin the carrier of R st
( bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i0) \ {(MinElement (rng Smax),R)} & bn . i0 = bni ) by A35;
A38: ex bni1 being Element of Fin the carrier of R st
( bni1 = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . (i + 1)) \ {(MinElement (rng Smax),R)} & bn . (i + 1) = bni1 ) by A35;
reconsider bnti = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i, bnti1 = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . (i + 1) as Element of ;
reconsider bnti' = bnti, bnti1' = bnti1 as Element of Fin the carrier of R ;
A39: bnti1 <> bnti by A36, WELLFND1:def 7;
[bnti1,bnti] in FinOrd R by A36, WELLFND1:def 7;
then consider x, y being Element of Fin the carrier of R such that
A40: bnti1 = x and
A41: bnti = y and
A42: ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ) by Th40;

A43: now

let i be Nat; :: thesis:
(Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i = Sn2 . (i + (Smax mindex (MinElement (rng Smax),R))) by NAT_1:def 3;
hence (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i <> {} by A5; :: thesis:

end;

A44: now

A45: ex bnti'' being Element of Fin the carrier of R st
( bnti'' = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i & PosetMax bnti'' = MinElement (rng Smax),R ) by A34;
ex bnti1'' being Element of Fin the carrier of R st
( bnti1'' = (Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . (i + 1) & PosetMax bnti1'' = MinElement (rng Smax),R ) by A34;
hence ( PosetMax bnti' = MinElement (rng Smax),R & PosetMax bnti1' = MinElement (rng Smax),R ) by A45; :: thesis:

end;

A46: bnti' <> {} by A43;
A47: bnti1' <> {} by A43;
A48: MinElement (rng Smax),R in bnti by A44, A46, Def15;
MinElement (rng Smax),R in bnti1 by A44, A47, Def15;
hence bn . (i + 1) <> bn . i by A37, A38, A39, A48, Th1; :: thesis:

per cases by A42;

suppose x = {} ; :: thesis:

hence [(bn . (i + 1)),(bn . i)] in FinOrd R by A40, A43; :: thesis:

end;

suppose ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of R ) ; :: thesis:

hence [(bn . (i + 1)),(bn . i)] in FinOrd R by A40, A41, A44; :: thesis:

end;

suppose ( x <> {} & y <> {} & PosetMax x = PosetMax y & [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ; :: thesis:

hence [(bn . (i + 1)),(bn . i)] in FinOrd R by A37, A38, A40, A41, A44; :: thesis:

end;

then bn is descending by WELLFND1:def 7;
then bn in zz ;
then reconsider Sn1 = [(MinElement (rng Smax),R),bn] as Element of [:the carrier of R,zz:] by ZFMISC_1:def 2;
take Sn1 ; :: thesis:
take Sn2 ; :: thesis:
take Smax ; :: thesis:
take MinElement (rng Smax),R ; :: thesis:
take Smax mindex (MinElement (rng Smax),R) ; :: thesis:
take Sn2 ^\ (Smax mindex (MinElement (rng Smax),R)) ; :: thesis:
take bn ; :: thesis:
thus Sn2 = Sn `2 ; :: thesis:
thus for i being Nat ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) :: thesis:

proof

let i be Nat; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i0 = PosetMax Sn2i ) by A9;
hence ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ; :: thesis:

end;

thus MinElement (rng Smax),R = MinElement (rng Smax),R ; :: thesis:
thus Smax mindex (MinElement (rng Smax),R) = Smax mindex (MinElement (rng Smax),R) ; :: thesis:
thus Sn2 ^\ (Smax mindex (MinElement (rng Smax),R)) = Sn2 ^\ (Smax mindex (MinElement (rng Smax),R)) ; :: thesis:

now

let i be Nat; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;
ex bni being Element of Fin the carrier of R st
( bni = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i0) \ {(MinElement (rng Smax),R)} & bn . i0 = bni ) by A35;
hence bn . i = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i) \ {(MinElement (rng Smax),R)} ; :: thesis:

end;

hence for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement (rng Smax),R))) . i) \ {(MinElement (rng Smax),R)} ; :: thesis:
thus for i being Nat st Smax mindex (MinElement (rng Smax),R) <= i holds
Smax . i = MinElement (rng Smax),R by A28; :: thesis:
thus Sn1 = [(MinElement (rng Smax),R),bn] ; :: thesis:

end;

consider aStart being Element of ;
set SS = [aStart,A];
A in zz by A2;
then reconsider SS = [aStart,A] as Element of [:the carrier of R,zz:] by ZFMISC_1:def 2;
consider S01 being Element of [:the carrier of R,zz:], S02 being sequence of (FinPoset R), S0max being Function of NAT ,the carrier of R, a0 being Element of , i0 being Nat, b0t, b0 being sequence of (FinPoset R) such that
S02 = SS `2 and
A49: for i being Nat ex S02i being Element of Fin the carrier of R st
( S02i = S02 . i & S02i <> {} & S0max . i = PosetMax S02i ) and
a0 = MinElement (rng S0max),R and
i0 = S0max mindex a0 and
A50: b0t = S02 ^\ i0 and
A51: for i being Nat holds b0 . i = (b0t . i) \ {a0} and
A52: for i being Nat st i0 <= i holds
S0max . i = a0 and
A53: S01 = [a0,b0] by A3;
consider S being Function of NAT ,[:the carrier of R,zz:] such that
A54: S . 0 = S01 and
A55: for n being Element of NAT holds S₁[n,S . n,S . (n + 1)] from RECDEF_1:sch 2(A3);
B55: for n being Nat holds S₁[n,S . n,S . (n + 1)]

proof

let n be Nat; :: thesis:
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;
S₁[n0,S . n0,S . (n0 + 1)] by A55;
hence S₁[n,S . n,S . (n + 1)] ; :: thesis:

end;

deffunc H₁( set ) -> set = (S . $1) `1 ;

A56: now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x' = x as Nat ;
reconsider Sx = S . x' as Element of [:the carrier of R,zz:] ;
Sx `1 in the carrier of R ;
hence H₁(x) in the carrier of R ; :: thesis:

end;

consider a being Function of NAT ,the carrier of R such that
A57: for x being set st x in NAT holds
a . x = H₁(x) from FUNCT_2:sch 2(A56);
reconsider a = a as sequence of R ;
defpred S₂[ Nat] means for i being Nat ex b being sequence of (FinPoset R) st
( b = (S . $1) `2 & ( for x being set st x in b . i holds
( x <> (S . $1) `1 & [x,((S . $1) `1 )] in the InternalRel of R ) ) );
A58: S₂[ 0 ]

proof

let i be Nat; :: thesis:
set b = (S . 0 ) `2 ;
(S . 0 ) `2 in zz ;
then ex z being sequence of (FinPoset R) st
( z = (S . 0 ) `2 & z is descending ) ;
then reconsider b = (S . 0 ) `2 as sequence of (FinPoset R) ;
take b ; :: thesis:
thus b = (S . 0 ) `2 ; :: thesis:
let x be set ; :: thesis:
assume A59: x in b . i ; :: thesis:
A60: a0 = (S . 0 ) `1 by A53, A54, MCART_1:def 1;
b0 = b by A53, A54, MCART_1:def 2;
then A61: x in (b0t . i) \ {a0} by A51, A59;
then A62: x in b0t . i ;
not x in {a0} by A61, XBOOLE_0:def 5;
hence A63: x <> (S . 0 ) `1 by A60, TARSKI:def 1; :: thesis:
b . i c= the carrier of R by FINSUB_1:def 5;
then reconsider x' = x as Element of by A59;
A64: x in S02 . (i + i0) by A50, A62, NAT_1:def 3;
consider S02ib being Element of Fin the carrier of R such that
A65: S02ib = S02 . (i + i0) and
A66: S02ib <> {} and
A67: S0max . (i + i0) = PosetMax S02ib by A49;
PosetMax S02ib = a0 by A52, A67, NAT_1:11;
then a0 is_maximal_wrt S02ib,the InternalRel of R by A66, Def15;
then not [a0,x] in the InternalRel of R by A60, A63, A64, A65, WAYBEL_4:def 24;
then not a0 <= x' by ORDERS_2:def 9;
then x' <= a0 by WAYBEL_0:def 29;
hence [x,((S . 0 ) `1 )] in the InternalRel of R by A60, ORDERS_2:def 9; :: thesis:

end;

A68: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume S₂[n] ; :: thesis:
let i be Nat; :: thesis:
set n1 = n + 1;
reconsider n1 = n + 1 as Nat ;
set b = (S . n1) `2 ;
consider Sn2 being sequence of (FinPoset R), Smax being Function of NAT ,the carrier of R, an being Element of , ix being Nat, bnt, bn being sequence of (FinPoset R) such that
Sn2 = (S . n) `2 and
A69: for i being Nat ex Sn2i being Element of Fin the carrier of R st
( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) and
an = MinElement (rng Smax),R and
ix = Smax mindex an and
A70: bnt = Sn2 ^\ ix and
A71: for i being Nat holds bn . i = (bnt . i) \ {an} and
A72: for i being Nat st ix <= i holds
Smax . i = an and
A73: S . (n + 1) = [an,bn] by B55;
(S . n1) `2 in zz ;
then ex z being sequence of (FinPoset R) st
( z = (S . n1) `2 & z is descending ) ;
then reconsider b = (S . n1) `2 as sequence of (FinPoset R) ;
take b ; :: thesis:
thus b = (S . (n + 1)) `2 ; :: thesis:
let x be set ; :: thesis:
assume A74: x in b . i ; :: thesis:
A75: an = (S . n1) `1 by A73, MCART_1:def 1;
bn = b by A73, MCART_1:def 2;
then A76: x in (bnt . i) \ {an} by A71, A74;
then A77: x in bnt . i ;
not x in {an} by A76, XBOOLE_0:def 5;
hence A78: x <> (S . (n + 1)) `1 by A75, TARSKI:def 1; :: thesis:
b . i c= the carrier of R by FINSUB_1:def 5;
then reconsider x' = x as Element of by A74;
A79: x in Sn2 . (i + ix) by A70, A77, NAT_1:def 3;
consider Sn2ib being Element of Fin the carrier of R such that
A80: Sn2ib = Sn2 . (i + ix) and
A81: Sn2ib <> {} and
A82: Smax . (i + ix) = PosetMax Sn2ib by A69;
PosetMax Sn2ib = an by A72, A82, NAT_1:11;
then an is_maximal_wrt Sn2ib,the InternalRel of R by A81, Def15;
then not [an,x] in the InternalRel of R by A75, A78, A79, A80, WAYBEL_4:def 24;
then not an <= x' by ORDERS_2:def 9;
then x' <= an by WAYBEL_0:def 29;
hence [x,((S . (n + 1)) `1 )] in the InternalRel of R by A75, ORDERS_2:def 9; :: thesis:

end;

A83: for n being Nat holds S₂[n] from NAT_1:sch 2(A58, A68);
defpred S₃[ Nat] means ex b being sequence of (FinPoset R) ex i being Nat st
( b = (S . $1) `2 & a . ($1 + 1) in b . i );
A84: S₃[ 0 ]

proof

set b = (S . 0 ) `2 ;
(S . 0 ) `2 in zz ;
then ex z being sequence of (FinPoset R) st
( z = (S . 0 ) `2 & z is descending ) ;
then reconsider b = (S . 0 ) `2 as sequence of (FinPoset R) ;
take b ; :: thesis:
A85: a . (0 + 1) = (S . (0 + 1)) `1 by A57;
consider S12 being sequence of (FinPoset R), S1max being Function of NAT ,the carrier of R, a1 being Element of , i1 being Nat, b1t, b1 being sequence of (FinPoset R) such that
A86: S12 = (S . 0 ) `2 and
A87: for i being Nat ex S12i being Element of Fin the carrier of R st
( S12i = S12 . i & S12i <> {} & S1max . i = PosetMax S12i ) and
A88: a1 = MinElement (rng S1max),R and
i1 = S1max mindex a1 and
b1t = S12 ^\ i1 and
for i being Nat holds b1 . i = (b1t . i) \ {a1} and
for i being Nat st i1 <= i holds
S1max . i = a1 and
A89: S . (0 + 1) = [a1,b1] by A55;
rng S1max c= the carrier of R by RELAT_1:def 19;
then a1 in rng S1max by A1, A88, Def19;
then consider i being set such that
A90: i in dom S1max and
A91: S1max . i = a1 by FUNCT_1:def 5;
A92: ex S12i being Element of Fin the carrier of R st
( S12i = S12 . i & S12i <> {} & S1max . i = PosetMax S12i ) by A87, A90;
reconsider i = i as Nat by A90;
take i ; :: thesis:
thus b = (S . 0 ) `2 ; :: thesis:
a1 in b . i by A86, A91, A92, Def15;
hence a . (0 + 1) in b . i by A85, A89, MCART_1:def 1; :: thesis:

end;

A93: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis:
assume S₃[n] ; :: thesis:
set b = (S . (n + 1)) `2 ;
(S . (n + 1)) `2 in zz ;
then ex z being sequence of (FinPoset R) st
( z = (S . (n + 1)) `2 & z is descending ) ;
then reconsider b = (S . (n + 1)) `2 as sequence of (FinPoset R) ;
take b ; :: thesis:
set n1 = n + 1;
reconsider n1 = n + 1 as Nat ;
consider Sn12 being sequence of (FinPoset R), Sn1max being Function of NAT ,the carrier of R, an1 being Element of , in1 being Nat, bn1t, bn1 being sequence of (FinPoset R) such that
A94: Sn12 = (S . n1) `2 and
A95: for i being Nat ex Sn12i being Element of Fin the carrier of R st
( Sn12i = Sn12 . i & Sn12i <> {} & Sn1max . i = PosetMax Sn12i ) and
A96: an1 = MinElement (rng Sn1max),R and
in1 = Sn1max mindex an1 and
bn1t = Sn12 ^\ in1 and
for i being Nat holds bn1 . i = (bn1t . i) \ {an1} and
for i being Nat st in1 <= i holds
Sn1max . i = an1 and
A97: S . (n1 + 1) = [an1,bn1] by A55;
rng Sn1max c= the carrier of R by RELAT_1:def 19;
then an1 in rng Sn1max by A1, A96, Def19;
then consider i being set such that
A98: i in dom Sn1max and
A99: Sn1max . i = an1 by FUNCT_1:def 5;
A100: ex Sn12i being Element of Fin the carrier of R st
( Sn12i = Sn12 . i & Sn12i <> {} & Sn1max . i = PosetMax Sn12i ) by A95, A98;
reconsider i = i as Nat by A98;
take i ; :: thesis:
thus b = (S . (n + 1)) `2 ; :: thesis:
A101: an1 in b . i by A94, A99, A100, Def15;
(S . (n1 + 1)) `1 = an1 by A97, MCART_1:def 1;
hence a . ((n + 1) + 1) in b . i by A57, A101; :: thesis:

end;

A102: for n being Nat holds S₃[n] from NAT_1:sch 2(A84, A93);
defpred S₄[ Nat] means ( a . ($1 + 1) <> a . $1 & [(a . ($1 + 1)),(a . $1)] in the InternalRel of R );
A103: S₄[ 0 ]

proof

A104: a . 0 = (S . 0 ) `1 by A57;
consider b being sequence of (FinPoset R), i being Nat such that
A105: b = (S . 0 ) `2 and
A106: a . (0 + 1) in b . i by A84;
ex bb being sequence of (FinPoset R) st
( bb = (S . 0 ) `2 & ( for x being set st x in bb . i holds
( x <> (S . 0 ) `1 & [x,((S . 0 ) `1 )] in the InternalRel of R ) ) ) by A58;
hence ( a . (0 + 1) <> a . 0 & [(a . (0 + 1)),(a . 0 )] in the InternalRel of R ) by A104, A105, A106; :: thesis:

end;

A107: for n being Nat st S₄[n] holds
S₄[n + 1]

proof

let n be Nat; :: thesis:
assume that
a . (n + 1) <> a . n and
[(a . (n + 1)),(a . n)] in the InternalRel of R ; :: thesis:
A108: a . (n + 1) = (S . (n + 1)) `1 by A57;
consider b being sequence of (FinPoset R), i being Nat such that
A109: b = (S . (n + 1)) `2 and
A110: a . ((n + 1) + 1) in b . i by A102;
ex bb being sequence of (FinPoset R) st
( bb = (S . (n + 1)) `2 & ( for x being set st x in bb . i holds
( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1 )] in the InternalRel of R ) ) ) by A83;
hence S₄[n + 1] by A108, A109, A110; :: thesis:

end;

for n being Nat holds S₄[n] from NAT_1:sch 2(A103, A107);
then a is descending by WELLFND1:def 7;
hence contradiction by A1, WELLFND1:15; :: thesis: