defpred S₁[ Ordinal] means InvLexOrder $1 is well-ordering ;

let o be Ordinal; :: thesis:
assume A2: for n being Ordinal st n in o holds
S₁[n] ; :: thesis:
set ilo = InvLexOrder o;
A3: InvLexOrder o is_strongly_connected_in Bags o by Def5;
then InvLexOrder o is_reflexive_in Bags o ;
then A4: field (InvLexOrder o) = Bags o by PARTIT_2:9;

assume not InvLexOrder o is well_founded ; :: thesis:
then A6: not InvLexOrder o is_well_founded_in Bags o by A4, WELLORD1:3;
set R = RelStr(# (Bags o),(InvLexOrder o) #);
set ir = the InternalRel of RelStr(# (Bags o),(InvLexOrder o) #);
not RelStr(# (Bags o),(InvLexOrder o) #) is well_founded by A6;
then consider f being sequence of RelStr(# (Bags o),(InvLexOrder o) #) such that
A7: f is descending by WELLFND1:14;
reconsider a = f . 0 as bag of o ;
set s = SgmX ((RelIncl o),(support a));
A8: field (RelIncl o) = o by WELLORD2:def 1;
RelIncl o is being_linear-order by ORDERS_1:19;
then A9: RelIncl o linearly_orders support a by A8, ORDERS_1:37, ORDERS_1:38;
then A10: rng (SgmX ((RelIncl o),(support a))) = support a by PRE_POLY:def 2;

now :: thesis:

assume rng (SgmX ((RelIncl o),(support a))) = {} ; :: thesis:
then A11: a = EmptyBag o by A10, PRE_POLY:81;
reconsider b = f . (0 + 1) as bag of o ;
A12: b <> a by A7;
[b,a] in the InternalRel of RelStr(# (Bags o),(InvLexOrder o) #) by A7;
then ex i being Ordinal st
( i in o & b . i < a . i & ( for k being Ordinal st i in k & k in o holds
b . k = a . k ) ) by A12, Def6;
hence contradiction by A11, PBOOLE:5; :: thesis:

end;

then A13: len (SgmX ((RelIncl o),(support a))) in dom (SgmX ((RelIncl o),(support a))) by FINSEQ_5:6, RELAT_1:38;
then A14: (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) in rng (SgmX ((RelIncl o),(support a))) by FUNCT_1:3;
then reconsider j = (SgmX ((RelIncl o),(support a))) . (len (SgmX ((RelIncl o),(support a)))) as Ordinal by A10;
defpred S₂[ set , set ] means ex b being bag of o st
( f . $1 = b & $2 = b . j );

A15: now :: thesis:

let x be Element of NAT ; :: thesis:
reconsider b = f . x as bag of o ;
take y = b . j; :: thesis:
thus S₂[x,y] ; :: thesis:

end;

consider t being sequence of NAT such that
A16: for i being Element of NAT holds S₂[i,t . i] from FUNCT_2:sch 3(A15);
defpred S₃[ Nat] means for i being Ordinal
for b being bag of o st j in i & i in o & f . $1 = b holds
b . i = 0 ;
A17: S₃[ 0 ]

proof

let i be Ordinal; :: thesis:
let b be bag of o; :: thesis:
assume that
A18: j in i and
A19: i in o and
A20: f . 0 = b ; :: thesis:
assume b . i <> 0 ; :: thesis:
then i in support a by A20, PRE_POLY:def 7;
then consider k being Nat such that
A21: k in dom (SgmX ((RelIncl o),(support a))) and
A22: (SgmX ((RelIncl o),(support a))) . k = i by A10, FINSEQ_2:10;
A23: k <= len (SgmX ((RelIncl o),(support a))) by A21, FINSEQ_3:25;

per cases by A23, XXREAL_0:1;

suppose k = len (SgmX ((RelIncl o),(support a))) ; :: thesis:

hence contradiction by A18, A22; :: thesis:

end;

suppose k < len (SgmX ((RelIncl o),(support a))) ; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume A25: for i being Ordinal
for b being bag of o st j in i & i in o & f . n = b holds
b . i = 0 ; :: thesis:
let i be Ordinal; :: thesis:
let b1 be bag of o; :: thesis:
assume that
A26: j in i and
A27: i in o and
A28: f . (n + 1) = b1 ; :: thesis:
reconsider b = f . n as bag of o ;
A29: b . i = 0 by A25, A26, A27;
A30: b1 <> b by A7, A28;
[b1,b] in InvLexOrder o by A7, A28;
then consider i1 being Ordinal such that
A31: i1 in o and
A32: b1 . i1 < b . i1 and
A33: for k being Ordinal st i1 in k & k in o holds
b1 . k = b . k by A30, Def6;

per cases by ORDINAL1:14;

suppose i1 in i ; :: thesis:

hence b1 . i = 0 by A27, A29, A33; :: thesis:

end;

suppose i1 = i ; :: thesis:

hence b1 . i = 0 by A25, A26, A27, A32; :: thesis:

end;

suppose A34: i in i1 ; :: thesis:

assume b1 . i <> 0 ; :: thesis:
j in i1 by A26, A34, ORDINAL1:10;
hence contradiction by A25, A31, A32; :: thesis:

end;

A35: for n being Nat holds S₃[n] from NAT_1:sch 2(A17, A24);
reconsider t = t as sequence of OrderedNAT by DICKSON:def 15;
A36: t is non-increasing

proof

let n be Nat; :: according to BAGORDER:def 3 :: thesis:
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
reconsider tn = t . n0, tn1 = t . (n0 + 1) as Nat ;
reconsider fn = f . n0, fn1 = f . (n0 + 1) as bag of o ;
A37: fn1 <> fn by A7;
[fn1,fn] in InvLexOrder o by A7;
then consider i being Ordinal such that
A38: i in o and
A39: fn1 . i < fn . i and
A40: for k being Ordinal st i in k & k in o holds
fn1 . k = fn . k by A37, Def6;
A41: ex bn being bag of o st
( fn = bn & tn = bn . j ) by A16;
A42: ex bn1 being bag of o st
( fn1 = bn1 & tn1 = bn1 . j ) by A16;

now :: thesis:

per cases by ORDINAL1:14;

suppose i = j ; :: thesis:

hence tn1 <= tn by A39, A41, A42; :: thesis:

end;

suppose j in i ; :: thesis:

hence tn1 <= tn by A35, A38, A39; :: thesis:

end;

suppose i in j ; :: thesis:

hence tn1 <= tn by A10, A14, A40, A41, A42; :: thesis:

end;

hence [(t . (n + 1)),(t . n)] in the InternalRel of OrderedNAT by DICKSON:def 14, DICKSON:def 15; :: thesis:

end;

set n = j;
set iln = InvLexOrder j;
set S = RelStr(# (Bags j),(InvLexOrder j) #);
InvLexOrder j is_strongly_connected_in Bags j by Def5;
then InvLexOrder j is_reflexive_in Bags j ;
then A43: field (InvLexOrder j) = Bags j by PARTIT_2:9;
consider p being Nat such that
A44: for r being Nat st p <= r holds
t . p = t . r by A36, Th9;
defpred S₄[ Nat, set ] means ex b being bag of o st
( b = f . (p + $1) & $2 = b | j );

A45: now :: thesis:

let x be Element of NAT ; :: thesis:
reconsider b = f . (p + x) as bag of o ;
reconsider y = b | j as bag of j by A10, A14, Th17;
reconsider y = y as Element of Bags j by PRE_POLY:def 12;
take y = y; :: thesis:
thus S₄[x,y] ; :: thesis:

end;

consider g being sequence of (Bags j) such that
A46: for x being Element of NAT holds S₄[x,g . x] from FUNCT_2:sch 3(A45);
reconsider g = g as sequence of RelStr(# (Bags j),(InvLexOrder j) #) ;

now :: thesis:

let k be Nat; :: thesis:
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
consider b being bag of o such that
A47: b = f . (p + k) and
A48: g . k0 = b | j by A46;
consider b1 being bag of o such that
A49: b1 = f . (p + (k + 1)) and
A50: g . (k + 1) = b1 | j by A46;
p + (k + 1) = (p + k) + 1 ;
then A51: b <> b1 by A7, A47, A49;
A52: ex bb being bag of o st
( f . (p + k) = bb & t . (p + k0) = bb . j ) by A16;
A53: ex bb1 being bag of o st
( f . (p + (k + 1)) = bb1 & t . (p + (k + 1)) = bb1 . j ) by A16;
A54: t . (p + k) = t . p by A44, NAT_1:11;
thus g . (k + 1) <> g . k :: thesis:

proof

assume A55: not g . (k + 1) <> g . k ; :: thesis:
A56: o = dom b by PARTFUN1:def 2;
A57: o = dom b1 by PARTFUN1:def 2;

now :: thesis:

let m be object ; :: thesis:
assume A58: m in o ; :: thesis:
reconsider mm = m as set by TARSKI:1;

per cases by A58, ORDINAL1:14;

suppose A59: m in j ; :: thesis:

then (b | j) . m = b . m by FUNCT_1:49;
hence b . m = b1 . m by A48, A50, A55, A59, FUNCT_1:49; :: thesis:

end;

suppose m = j ; :: thesis:

hence b . m = b1 . m by A44, A47, A49, A52, A53, A54, NAT_1:11; :: thesis:

end;

suppose A60: j in mm ; :: thesis:

then b . m = 0 by A35, A47, A58;
hence b . m = b1 . m by A35, A49, A58, A60; :: thesis:

end;

hence contradiction by A51, A56, A57, FUNCT_1:2; :: thesis:

end;

[(f . ((p + k) + 1)),(f . (p + k))] in InvLexOrder o by A7;
then consider i being Ordinal such that
A61: i in o and
A62: b1 . i < b . i and
A63: for k being Ordinal st i in k & k in o holds
b . k = b1 . k by A47, A49, A51, Def6;

A64: now :: thesis:

assume A65: not i in j ; :: thesis:

per cases by A65, ORDINAL1:14;

suppose i = j ; :: thesis:

hence contradiction by A44, A47, A49, A52, A53, A54, A62, NAT_1:11; :: thesis:

end;

suppose A66: j in i ; :: thesis:

then b . i = 0 by A35, A47, A61
.= b1 . i by A35, A49, A61, A66 ;
hence contradiction by A62; :: thesis:

end;

reconsider bj = b | j, b1j = b1 | j as bag of j by A10, A14, Th17;
A67: b1j . i = b1 . i by A64, FUNCT_1:49;
A68: bj . i = b . i by A64, FUNCT_1:49;

now :: thesis:

let k be Ordinal; :: thesis:
assume that
A69: i in k and
A70: k in j ; :: thesis:
k in o by A10, A14, A70, ORDINAL1:10;
then A71: b . k = b1 . k by A63, A69;
thus bj . k = b . k by A70, FUNCT_1:49
.= b1j . k by A70, A71, FUNCT_1:49 ; :: thesis:

end;

hence [(g . (k + 1)),(g . k)] in InvLexOrder j by A48, A50, A62, A64, A67, A68, Def6; :: thesis:

end;

then g is descending ;
then not RelStr(# (Bags j),(InvLexOrder j) #) is well_founded by WELLFND1:14;
then not InvLexOrder j is_well_founded_in the carrier of RelStr(# (Bags j),(InvLexOrder j) #) ;
then not InvLexOrder j well_orders field (InvLexOrder j) by A43, WELLORD1:def 5;
then not InvLexOrder j is well-ordering by WELLORD1:4;
hence contradiction by A2, A10, A14; :: thesis:

end;

A72: field (InvLexOrder o) = Bags o by ORDERS_1:12;
then A73: InvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;
A74: InvLexOrder o is_transitive_in Bags o by A72, RELAT_2:def 16;
A75: InvLexOrder o is_antisymmetric_in Bags o by A72, RELAT_2:def 12;
A76: InvLexOrder o is_connected_in field (InvLexOrder o) by A3, A4;
InvLexOrder o is_well_founded_in field (InvLexOrder o) by A5, WELLORD1:3;
then InvLexOrder o well_orders field (InvLexOrder o) by A4, A73, A74, A75, A76, WELLORD1:def 5;
hence S₁[o] by WELLORD1:4; :: thesis:

end;

thus for o being Ordinal holds S₁[o] from ORDINAL1:sch 2(A1); :: thesis: