let R be non empty connected Poset; :: thesis: ( R is well_founded implies FinPoset R is well_founded )

assume A1: R is well_founded ; :: thesis: FinPoset R is well_founded

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

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_{1}[ 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_{1}[n,Sn,Sn1]

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_{1}[n,S . n,S . (n + 1)]
from RECDEF_1:sch 2(A3);

A56: for n being Nat holds S_{1}[n,S . n,S . (n + 1)]
by A55;

deffunc H_{1}( object ) -> object = (S . $1) `1 ;

A58: for x being object st x in NAT holds

a . x = H_{1}(x)
from FUNCT_2:sch 2(A57);

reconsider a = a as sequence of R ;

defpred S_{2}[ 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_{2}[ 0 ]
_{2}[n] holds

S_{2}[n + 1]
_{2}[n]
from NAT_1:sch 2(A59, A68);

defpred S_{3}[ 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_{3}[ 0 ]
_{3}[n] holds

S_{3}[n + 1]
_{3}[n]
from NAT_1:sch 2(A83, A93);

defpred S_{4}[ Nat] means ( a . ($1 + 1) <> a . $1 & [(a . ($1 + 1)),(a . $1)] in the InternalRel of R );

A103: S_{4}[ 0 ]
_{4}[n] holds

S_{4}[n + 1]
_{4}[n]
from NAT_1:sch 2(A103, A107);

then a is descending ;

hence contradiction by A1, WELLFND1:14; :: thesis: verum

assume A1: R is well_founded ; :: thesis: FinPoset R is well_founded

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

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

( 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

proof

set aStart = the Element of R;
let n be Nat; :: thesis: for Sn being Element of [: the carrier of R,zz:] ex Sn1 being Element of [: the carrier of R,zz:] st S_{1}[n,Sn,Sn1]

let Sn be Element of [: the carrier of R,zz:]; :: thesis: ex Sn1 being Element of [: the carrier of R,zz:] st S_{1}[n,Sn,Sn1]

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) ;

_{2}[ 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_{2}[i,y]

A9: for i being Element of NAT holds S_{2}[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_{3}[ 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 );

_{3}[i,y]
;

defpred S_{4}[ 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_{4}[ 0 ]
by A11, A13, DICKSON:def 11;

_{4}[k]
from NAT_1:sch 2(A15, A16);

A35: for i being Element of NAT holds S_{3}[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;

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: S_{1}[n,Sn,Sn1]

take Sn2 ; :: thesis: 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 = Sn `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 ) & Sn1 = [an,bn] )

take Smax ; :: thesis: ex an being Element of R ex ix being Nat ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `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 ) & Sn1 = [an,bn] )

take MinElement ((rng Smax),R) ; :: thesis: ex ix being Nat ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & ix = Smax mindex (MinElement ((rng Smax),R)) & bnt = Sn2 ^\ ix & ( for i being Nat holds bn . i = (bnt . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st ix <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take Smax mindex (MinElement ((rng Smax),R)) ; :: thesis: ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & bnt = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = (bnt . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) ; :: thesis: ex bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take bn ; :: thesis: ( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Sn2 = Sn `2 ; :: thesis: ( ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

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: ( MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) ; :: thesis: ( Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) ; :: thesis: ( ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) by A28; :: thesis: Sn1 = [(MinElement ((rng Smax),R)),bn]

thus Sn1 = [(MinElement ((rng Smax),R)),bn] ; :: thesis: verum

end;let Sn be Element of [: the carrier of R,zz:]; :: thesis: ex Sn1 being Element of [: the carrier of R,zz:] st S

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 :: thesis: for i being Nat holds not Sn2 . i = {}

defpred Slet i be Nat; :: thesis: not Sn2 . i = {}

assume A6: Sn2 . i = {} ; :: thesis: contradiction

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

end;assume A6: Sn2 . i = {} ; :: thesis: contradiction

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

( 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

proof

consider Smax being sequence of the carrier of R such that
let i be Element of NAT ; :: thesis: ex y being Element of the carrier of R st S_{2}[i,y]

set Sn2i = Sn2 . i;

reconsider Sn2i = Sn2 . i as Element of Fin the carrier of R ;

set y = PosetMax Sn2i;

take PosetMax Sn2i ; :: thesis: S_{2}[i, PosetMax Sn2i]

take Sn2i ; :: thesis: ( Sn2i = Sn2 . i & Sn2i <> {} & PosetMax Sn2i = PosetMax Sn2i )

thus Sn2i = Sn2 . i ; :: thesis: ( Sn2i <> {} & PosetMax Sn2i = PosetMax Sn2i )

thus Sn2i <> {} by A5; :: thesis: PosetMax Sn2i = PosetMax Sn2i

thus PosetMax Sn2i = PosetMax Sn2i ; :: thesis: verum

end;set Sn2i = Sn2 . i;

reconsider Sn2i = Sn2 . i as Element of Fin the carrier of R ;

set y = PosetMax Sn2i;

take PosetMax Sn2i ; :: thesis: S

take Sn2i ; :: thesis: ( Sn2i = Sn2 . i & Sn2i <> {} & PosetMax Sn2i = PosetMax Sn2i )

thus Sn2i = Sn2 . i ; :: thesis: ( Sn2i <> {} & PosetMax Sn2i = PosetMax Sn2i )

thus Sn2i <> {} by A5; :: thesis: PosetMax Sn2i = PosetMax Sn2i

thus PosetMax Sn2i = PosetMax Sn2i ; :: thesis: verum

A9: for i being Element of NAT holds S

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

( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . $1) \ {(MinElement ((rng Smax),R))} & $2 = bni );

now :: thesis: for i being Nat ex y, bni being Element of Fin the carrier of R st

( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

then A10:
for i being Element of NAT ex y being Element of Fin the carrier of R st S( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

let i be Nat; :: thesis: ex y, bni being Element of Fin the carrier of R st

( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

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: ex bni being Element of Fin the carrier of R st

( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

take bni = bni; :: thesis: ( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

thus bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ; :: thesis: y = bni

thus y = bni ; :: thesis: verum

end;( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

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: ex bni being Element of Fin the carrier of R st

( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

take bni = bni; :: thesis: ( bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} & y = bni )

thus bni = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ; :: thesis: y = bni

thus y = bni ; :: thesis: verum

defpred S

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

A16: now :: thesis: for k being Nat st S_{4}[k] holds

S_{4}[k + 1]

A27:
for k being Nat holds SS

let k be Nat; :: thesis: ( S_{4}[k] implies S_{4}[b_{1} + 1] )

assume A17: S_{4}[k]
; :: thesis: S_{4}[b_{1} + 1]

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;

end;assume A17: S

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
( 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 A25;

end;

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

Smax . ((Smax mindex (MinElement ((rng Smax),R))) + (k + 1)) in rng Smax
by A11, FUNCT_1:def 3;

hence S_{4}[k + 1]
by A14, A17, A19, A22, A23, A24, A26, WAYBEL_4:def 25; :: thesis: verum

end;hence S

A28: now :: thesis: for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R)

Smax . i = MinElement ((rng Smax),R)

let i be Nat; :: thesis: ( Smax mindex (MinElement ((rng Smax),R)) <= i implies Smax . i = MinElement ((rng Smax),R) )

assume Smax mindex (MinElement ((rng Smax),R)) <= i ; :: thesis: Smax . i = MinElement ((rng Smax),R)

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

end;assume Smax mindex (MinElement ((rng Smax),R)) <= i ; :: thesis: Smax . i = MinElement ((rng Smax),R)

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

A30: now :: thesis: for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

let i be Nat; :: thesis: ( Smax mindex (MinElement ((rng Smax),R)) <= i implies ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) ) )

assume A31: Smax mindex (MinElement ((rng Smax),R)) <= i ; :: thesis: ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

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: ( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

thus Sn2i = Sn2 . i by A32; :: thesis: PosetMax Sn2i = MinElement ((rng Smax),R)

thus PosetMax Sn2i = MinElement ((rng Smax),R) by A28, A31, A33; :: thesis: verum

end;( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) ) )

assume A31: Smax mindex (MinElement ((rng Smax),R)) <= i ; :: thesis: ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

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: ( Sn2i = Sn2 . i & PosetMax Sn2i = MinElement ((rng Smax),R) )

thus Sn2i = Sn2 . i by A32; :: thesis: PosetMax Sn2i = MinElement ((rng Smax),R)

thus PosetMax Sn2i = MinElement ((rng Smax),R) by A28, A31, A33; :: thesis: verum

A34: now :: thesis: for i being Nat 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) )

consider bn being sequence of (Fin the carrier of R) such that ( bnti = (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i & PosetMax bnti = MinElement ((rng Smax),R) )

let i be Nat; :: thesis: 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) )

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: ( bnti = (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i & PosetMax bnti = MinElement ((rng Smax),R) )

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

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

end;( bnti = (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i & PosetMax bnti = MinElement ((rng Smax),R) )

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: ( bnti = (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i & PosetMax bnti = MinElement ((rng Smax),R) )

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

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

A35: for i being Element of NAT holds S

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: for i being Nat holds

( bn . (i + 1) <> bn . i & [(bn . (i + 1)),(bn . i)] in FinOrd R )

then
bn is descending
;( bn . (i + 1) <> bn . i & [(bn . (i + 1)),(bn . i)] in FinOrd R )

let i be Nat; :: thesis: ( bn . (i + 1) <> bn . i & [(bn . (b_{1} + 1)),(bn . b_{1})] in FinOrd R )

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;

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: [(bn . (b_{1} + 1)),(bn . b_{1})] in FinOrd R

end;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: for i being Nat holds (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i <> {}

let i be Nat; :: thesis: (Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i <> {}

(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: verum

end;(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: verum

A44: now :: thesis: ( PosetMax bnti9 = MinElement ((rng Smax),R) & PosetMax bnti19 = MinElement ((rng Smax),R) )

A46:
bnti9 <> {}
by A43;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: verum

end;( 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: verum

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: [(bn . (b

per cases
( 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 A42;

end;

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

take Sn2 ; :: thesis: 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 = Sn `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 ) & Sn1 = [an,bn] )

take Smax ; :: thesis: ex an being Element of R ex ix being Nat ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `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 ) & Sn1 = [an,bn] )

take MinElement ((rng Smax),R) ; :: thesis: ex ix being Nat ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & ix = Smax mindex (MinElement ((rng Smax),R)) & bnt = Sn2 ^\ ix & ( for i being Nat holds bn . i = (bnt . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st ix <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take Smax mindex (MinElement ((rng Smax),R)) ; :: thesis: ex bnt, bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & bnt = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = (bnt . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) ; :: thesis: ex bn being sequence of (FinPoset R) st

( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

take bn ; :: thesis: ( Sn2 = Sn `2 & ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Sn2 = Sn `2 ; :: thesis: ( ( for i being Nat ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i ) ) & MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

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: ( MinElement ((rng Smax),R) = MinElement ((rng Smax),R) & Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

proof

thus
MinElement ((rng Smax),R) = MinElement ((rng Smax),R)
; :: thesis: ( Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) & Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds
let i be Nat; :: thesis: ex Sn2i being Element of Fin the carrier of R st

( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i )

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

end;( Sn2i = Sn2 . i & Sn2i <> {} & Smax . i = PosetMax Sn2i )

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

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Smax mindex (MinElement ((rng Smax),R)) = Smax mindex (MinElement ((rng Smax),R)) ; :: thesis: ( Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) & ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) = Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R))) ; :: thesis: ( ( for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))} ) & ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

now :: thesis: for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))}

hence
for i being Nat holds bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))}
; :: thesis: ( ( for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds let i be Nat; :: thesis: bn . i = ((Sn2 ^\ (Smax mindex (MinElement ((rng Smax),R)))) . i) \ {(MinElement ((rng Smax),R))}

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

end;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: verum

Smax . i = MinElement ((rng Smax),R) ) & Sn1 = [(MinElement ((rng Smax),R)),bn] )

thus for i being Nat st Smax mindex (MinElement ((rng Smax),R)) <= i holds

Smax . i = MinElement ((rng Smax),R) by A28; :: thesis: Sn1 = [(MinElement ((rng Smax),R)),bn]

thus Sn1 = [(MinElement ((rng Smax),R)),bn] ; :: thesis: verum

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

A56: for n being Nat holds S

deffunc H

A57: now :: thesis: for x being object st x in NAT holds

H_{1}(x) in the carrier of R

consider a being sequence of the carrier of R such that H

let x be object ; :: thesis: ( x in NAT implies H_{1}(x) in the carrier of R )

assume x in NAT ; :: thesis: H_{1}(x) in the carrier of R

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_{1}(x) in the carrier of R
; :: thesis: verum

end;assume x in NAT ; :: thesis: H

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

A58: for x being object st x in NAT holds

a . x = H

reconsider a = a as sequence of R ;

defpred S

( 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

proof

A68:
for n being Nat st S
let i be Nat; :: thesis: ex b being sequence of (FinPoset R) st

( b = (S . 0) `2 & ( for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) ) )

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: ( b = (S . 0) `2 & ( for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) ) )

thus b = (S . 0) `2 ; :: thesis: for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R )

let x be set ; :: thesis: ( x in b . i implies ( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) )

assume A60: x in b . i ; :: thesis: ( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R )

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: [x,((S . 0) `1)] in the InternalRel of R

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

end;( b = (S . 0) `2 & ( for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) ) )

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: ( b = (S . 0) `2 & ( for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) ) )

thus b = (S . 0) `2 ; :: thesis: for x being set st x in b . i holds

( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R )

let x be set ; :: thesis: ( x in b . i implies ( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R ) )

assume A60: x in b . i ; :: thesis: ( x <> (S . 0) `1 & [x,((S . 0) `1)] in the InternalRel of R )

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: [x,((S . 0) `1)] in the InternalRel of R

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

S

proof

A82:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume S_{2}[n]
; :: thesis: S_{2}[n + 1]

let i be Nat; :: thesis: ex b being sequence of (FinPoset R) st

( b = (S . (n + 1)) `2 & ( for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) ) )

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: ( b = (S . (n + 1)) `2 & ( for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) ) )

thus b = (S . (n + 1)) `2 ; :: thesis: for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R )

let x be set ; :: thesis: ( x in b . i implies ( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) )

assume A74: x in b . i ; :: thesis: ( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R )

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: [x,((S . (n + 1)) `1)] in the InternalRel of R

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

end;assume S

let i be Nat; :: thesis: ex b being sequence of (FinPoset R) st

( b = (S . (n + 1)) `2 & ( for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) ) )

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: ( b = (S . (n + 1)) `2 & ( for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) ) )

thus b = (S . (n + 1)) `2 ; :: thesis: for x being set st x in b . i holds

( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R )

let x be set ; :: thesis: ( x in b . i implies ( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R ) )

assume A74: x in b . i ; :: thesis: ( x <> (S . (n + 1)) `1 & [x,((S . (n + 1)) `1)] in the InternalRel of R )

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: [x,((S . (n + 1)) `1)] in the InternalRel of R

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

defpred S

( b = (S . $1) `2 & a . ($1 + 1) in b . i );

A83: S

proof

A93:
for n being Nat st S
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: ex i being Nat st

( b = (S . 0) `2 & a . (0 + 1) in b . i )

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: ( b = (S . 0) `2 & a . (0 + 1) in b . i )

thus b = (S . 0) `2 ; :: thesis: a . (0 + 1) in b . i

A92: a1 in b . i by A85, A90, A91, Def13;

thus a . (0 + 1) in b . i by A84, A88, A92; :: thesis: verum

end;(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: ex i being Nat st

( b = (S . 0) `2 & a . (0 + 1) in b . i )

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: ( b = (S . 0) `2 & a . (0 + 1) in b . i )

thus b = (S . 0) `2 ; :: thesis: a . (0 + 1) in b . i

A92: a1 in b . i by A85, A90, A91, Def13;

thus a . (0 + 1) in b . i by A84, A88, A92; :: thesis: verum

S

proof

A102:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume S_{3}[n]
; :: thesis: S_{3}[n + 1]

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: ex i being Nat st

( b = (S . (n + 1)) `2 & a . ((n + 1) + 1) in b . i )

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: ( b = (S . (n + 1)) `2 & a . ((n + 1) + 1) in b . i )

thus b = (S . (n + 1)) `2 ; :: thesis: a . ((n + 1) + 1) in b . i

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

end;assume S

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: ex i being Nat st

( b = (S . (n + 1)) `2 & a . ((n + 1) + 1) in b . i )

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: ( b = (S . (n + 1)) `2 & a . ((n + 1) + 1) in b . i )

thus b = (S . (n + 1)) `2 ; :: thesis: a . ((n + 1) + 1) in b . i

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

defpred S

A103: S

proof

A107:
for n being Nat st S
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: verum

end;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: verum

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{4}[n] implies S_{4}[n + 1] )

assume that

a . (n + 1) <> a . n and

[(a . (n + 1)),(a . n)] in the InternalRel of R ; :: thesis: S_{4}[n + 1]

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_{4}[n + 1]
by A108, A109, A110; :: thesis: verum

end;assume that

a . (n + 1) <> a . n and

[(a . (n + 1)),(a . n)] in the InternalRel of R ; :: thesis: S

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

then a is descending ;

hence contradiction by A1, WELLFND1:14; :: thesis: verum