let o be infinite Ordinal; :: thesis: not LexOrder o is well-ordering
set R = LexOrder o;
set r = RelStr(# (Bags o),(LexOrder o) #);
set ir = the InternalRel of RelStr(# (Bags o),(LexOrder o) #);
set cr = the carrier of RelStr(# (Bags o),(LexOrder o) #);
assume LexOrder o is well-ordering ; :: thesis: contradiction
then A1: LexOrder o is well_founded ;
the carrier of RelStr(# (Bags o),(LexOrder o) #) = field the InternalRel of RelStr(# (Bags o),(LexOrder o) #) by ORDERS_1:15;
then the InternalRel of RelStr(# (Bags o),(LexOrder o) #) is_well_founded_in the carrier of RelStr(# (Bags o),(LexOrder o) #) by A1, WELLORD1:3;
then A2: RelStr(# (Bags o),(LexOrder o) #) is well_founded ;
defpred S₁[ set , set ] means $2 = (o --> 0) +* ($1,1);

A3: now :: thesis: for n being Element of NAT ex y being Element of the carrier of RelStr(# (Bags o),(LexOrder o) #) st S₁[n,y]

let n be Element of NAT ; :: thesis: ex y being Element of the carrier of RelStr(# (Bags o),(LexOrder o) #) st S₁[n,y]
set y = (o --> 0) +* (n,1);
A4: dom (o --> 0) = o by FUNCOP_1:13;
reconsider y = (o --> 0) +* (n,1) as ManySortedSet of o ;
A5: omega c= o by CARD_3:85;

now :: thesis: for x being object holds
( ( x in {n} implies y . x <> 0 ) & ( y . x <> 0 implies x in {n} ) )

let x be object ; :: thesis: ( ( x in {n} implies y . x <> 0 ) & ( y . x <> 0 implies x in {n} ) )

hereby :: thesis: ( y . x <> 0 implies x in {n} )

assume x in {n} ; :: thesis: y . x <> 0
then x = n by TARSKI:def 1;
hence y . x <> 0 by A4, A5, FUNCT_7:31; :: thesis: verum

end;

assume that
A6: y . x <> 0 and
A7: not x in {n} ; :: thesis: contradiction
x <> n by A7, TARSKI:def 1;
then A8: y . x = (o --> 0) . x by FUNCT_7:32;

per cases ( x in dom (o --> 0) or not x in dom (o --> 0) ) ;

suppose x in dom (o --> 0) ; :: thesis: contradiction

hence contradiction by A6, A8, FUNCOP_1:7; :: thesis: verum

end;

suppose not x in dom (o --> 0) ; :: thesis: contradiction

hence contradiction by A6, A8, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

then support y = {n} by PRE_POLY:def 7;
then y is finite-support by PRE_POLY:def 8;
then reconsider y = y as Element of the carrier of RelStr(# (Bags o),(LexOrder o) #) by PRE_POLY:def 12;
take y = y; :: thesis: S₁[n,y]
thus S₁[n,y] ; :: thesis: verum

end;

consider f being sequence of the carrier of RelStr(# (Bags o),(LexOrder o) #) such that
A9: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A3);
reconsider f = f as sequence of RelStr(# (Bags o),(LexOrder o) #) ;
f is descending

proof

let n be Nat; :: according to WELLFND1:def 6 :: thesis: ( not f . (n + 1) = f . n & [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(LexOrder o) #) )
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set fn1 = f . (n0 + 1);
set fn = f . n0;
A10: f . (n0 + 1) = (o --> 0) +* ((n + 1),1) by A9;
A11: f . n0 = (o --> 0) +* (n,1) by A9;
reconsider fn1 = f . (n0 + 1) as bag of o ;
reconsider fn = f . n0 as bag of o ;
A12: n0 in omega ;
A13: omega c= o by CARD_3:85;
n <> n + 1 ;
then A14: fn1 . n = (o --> 0) . n by A10, FUNCT_7:32
.= 0 by A12, A13, FUNCOP_1:7 ;
A15: dom (o --> 0) = o by FUNCOP_1:13;
then A16: fn . n = 1 by A11, A13, FUNCT_7:31;

now :: thesis: for l being Ordinal st l in n holds
fn1 . l = fn . l

let l be Ordinal; :: thesis: ( l in n implies fn1 . l = fn . l )
assume A17: l in n ; :: thesis: fn1 . l = fn . l
then A18: l <> n ;
n < n + 1 by NAT_1:13;
then n in { i where i is Nat : i < n0 + 1 } ;
then n in n + 1 by AXIOMS:4;
then n c= n + 1 by ORDINAL1:def 2;
then l in n + 1 by A17;
then l <> n + 1 ;
hence fn1 . l = (o --> 0) . l by A10, FUNCT_7:32
.= fn . l by A11, A18, FUNCT_7:32 ;
:: thesis: verum

end;

then A19: fn1 < fn by A14, A16, PRE_POLY:def 9;
thus f . (n + 1) <> f . n by A11, A13, A14, A15, FUNCT_7:31; :: thesis: [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(LexOrder o) #)
fn1 <=' fn by A19, PRE_POLY:def 10;
hence [(f . (n + 1)),(f . n)] in the InternalRel of RelStr(# (Bags o),(LexOrder o) #) by PRE_POLY:def 14; :: thesis: verum

end;

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