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:14;
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 sequence of the carrier of R ex an being Element of R 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 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 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) ;

let i be Nat; :: thesis:
assume A6: Sn2 . i = {} ; :: thesis:
A7: Sn2 . (i + 1) <> Sn2 . i by A4;
[(Sn2 . (i + 1)),(Sn2 . i)] in FinOrd R by A4;
hence contradiction by A6, A7, Th33; :: 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 sequence of 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 :: thesis:

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 the carrier of R 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, Def17;
A14: MinElement ((rng Smax),R) is_minimal_wrt rng Smax, the InternalRel of R by A1, A12, Def17;
A15: S₄[ 0 ] by A11, A13, DICKSON:def 11;

A16: now :: thesis:

let k be Nat; :: thesis:
assume A17: S₄[k] ; :: thesis:
reconsider ixk = (Smax mindex (MinElement ((rng Smax),R))) + k as Element of NAT by ORDINAL1:def 12;
set ixk1 = (Smax mindex (MinElement ((rng Smax),R))) + (k + 1);
set ixk19 = ((Smax mindex (MinElement ((rng Smax),R))) + k) + 1;
consider Sn2ixk being Element of Fin the carrier of R such that
A18: Sn2ixk = Sn2 . ixk and
Sn2ixk <> {} and
A19: Smax . ixk = 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 Sn2ixk9 = Sn2ixk, Sn2ixk19 = Sn2ixk1 as Element of (FinPoset R) ;
(Smax mindex (MinElement ((rng Smax),R))) + (k + 1) = ((Smax mindex (MinElement ((rng Smax),R))) + k) + 1 ;
then [Sn2ixk19,Sn2ixk9] in FinOrd R by A4, A18, A20;
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 Th36;

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 3;
hence S₄[k + 1] by A14, A17, A19, A22, A23, A24, A26, WAYBEL_4:def 25; :: 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 :: thesis:

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 ;
i = (Smax mindex (MinElement ((rng Smax),R))) + k by A29;
hence Smax . i = MinElement ((rng Smax),R) by A27; :: thesis:

end;

A30: now :: thesis:

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 12;
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 :: thesis:

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 sequence of (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, Th37;

now :: thesis:

let i be Nat; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
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 (FinPoset R) ;
reconsider bnti9 = bnti, bnti19 = bnti1 as Element of Fin the carrier of R ;
A39: bnti1 <> bnti by A36;
[bnti1,bnti] in FinOrd R by A36;
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 Th36;

A43: now :: thesis:

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 :: thesis:

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

end;

A46: bnti9 <> {} by A43;
A47: bnti19 <> {} by A43;
A48: MinElement ((rng Smax),R) in bnti by A44, A46, Def13;
MinElement ((rng Smax),R) in bnti1 by A44, A47, Def13;
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 ;
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 12;
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 :: thesis:

let i be Nat; :: thesis:
reconsider i0 = i as Element of NAT by ORDINAL1:def 12;
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;

set aStart = the Element of R;
set SS = [ the Element of R,A];
A in zz by A2;
then reconsider SS = [ the Element of R,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 sequence of the carrier of R, a0 being Element of R, 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 sequence of [: the carrier of R,zz:] such that
A54: S . 0 = S01 and
A55: for n being Nat holds S₁[n,S . n,S . (n + 1)] from RECDEF_1:sch 2(A3);
A56: for n being Nat holds S₁[n,S . n,S . (n + 1)] by A55;
deffunc H₁( object ) -> object = (S . $1) `1 ;

A57: now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Nat ;
reconsider Sx = S . x9 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 sequence of the carrier of R such that
A58: for x being object st x in NAT holds
a . x = H₁(x) from FUNCT_2:sch 2(A57);
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 ) ) );
A59: 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 A60: x in b . i ; :: thesis:
b0 = [a0,b0] `2
.= b by A53, A54 ;
then A61: x in (b0t . i) \ {a0} by A51, A60;
then A62: x in b0t . i ;
not x in {a0} by A61, XBOOLE_0:def 5;
hence A63: x <> (S . 0) `1 by A53, A54, TARSKI:def 1; :: thesis:
b . i c= the carrier of R by FINSUB_1:def 5;
then reconsider x9 = x as Element of R by A60;
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, Def13;
then not [a0,x] in the InternalRel of R by A63, A64, A65, A53, A54, WAYBEL_4:def 23;
then not a0 <= x9 by ORDERS_2:def 5;
then x9 <= a0 by WAYBEL_0:def 29;
hence [x,((S . 0) `1)] in the InternalRel of R by A53, A54, ORDERS_2:def 5; :: 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 sequence of the carrier of R, an being Element of R, 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 A56;
(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:
bn = [an,bn] `2
.= b by A73 ;
then A75: x in (bnt . i) \ {an} by A71, A74;
then A76: x in bnt . i ;
not x in {an} by A75, XBOOLE_0:def 5;
hence A77: x <> (S . (n + 1)) `1 by A73, TARSKI:def 1; :: thesis:
b . i c= the carrier of R by FINSUB_1:def 5;
then reconsider x9 = x as Element of R by A74;
A78: x in Sn2 . (i + ix) by A70, A76, NAT_1:def 3;
consider Sn2ib being Element of Fin the carrier of R such that
A79: Sn2ib = Sn2 . (i + ix) and
A80: Sn2ib <> {} and
A81: Smax . (i + ix) = PosetMax Sn2ib by A69;
PosetMax Sn2ib = an by A72, A81, NAT_1:11;
then an is_maximal_wrt Sn2ib, the InternalRel of R by A80, Def13;
then not [an,x] in the InternalRel of R by A77, A78, A79, A73, WAYBEL_4:def 23;
then not an <= x9 by ORDERS_2:def 5;
then x9 <= an by WAYBEL_0:def 29;
hence [x,((S . (n + 1)) `1)] in the InternalRel of R by A73, ORDERS_2:def 5; :: thesis:

end;

A82: for n being Nat holds S₂[n] from NAT_1:sch 2(A59, 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 );
A83: 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:
A84: a . (0 + 1) = (S . (0 + 1)) `1 by A58;
consider S12 being sequence of (FinPoset R), S1max being sequence of the carrier of R, a1 being Element of R, i1 being Nat, b1t, b1 being sequence of (FinPoset R) such that
A85: S12 = (S . 0) `2 and
A86: for i being Nat ex S12i being Element of Fin the carrier of R st
( S12i = S12 . i & S12i <> {} & S1max . i = PosetMax S12i ) and
A87: 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
A88: 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, A87, Def17;
then consider i being object such that
A89: i in dom S1max and
A90: S1max . i = a1 by FUNCT_1:def 3;
A91: ex S12i being Element of Fin the carrier of R st
( S12i = S12 . i & S12i <> {} & S1max . i = PosetMax S12i ) by A86, A89;
reconsider i = i as Nat by A89;
take i ; :: thesis:
thus b = (S . 0) `2 ; :: thesis:
A92: a1 in b . i by A85, A90, A91, Def13;
thus a . (0 + 1) in b . i by A84, A88, A92; :: 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 sequence of the carrier of R, an1 being Element of R, 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, Def17;
then consider i being object such that
A98: i in dom Sn1max and
A99: Sn1max . i = an1 by FUNCT_1:def 3;
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, Def13;
[an1,bn1] `1 = an1 ;
hence a . ((n + 1) + 1) in b . i by A58, A101, A97; :: thesis:

end;

A102: for n being Nat holds S₃[n] from NAT_1:sch 2(A83, 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 A58;
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 A83;
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 A59;
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 A58;
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 A82;
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 ;
hence contradiction by A1, WELLFND1:14; :: thesis: