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_{1}[ set , set ] means $2 = (o --> 0) +* ($1,1);

A9: for n being Element of NAT holds S_{1}[n,f . n]
from FUNCT_2:sch 3(A3);

reconsider f = f as sequence of RelStr(# (Bags o),(LexOrder o) #) ;

f is descending

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

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

consider f being sequence of the carrier of RelStr(# (Bags o),(LexOrder o) #) such that let n be Element of NAT ; :: thesis: ex y being Element of the carrier of RelStr(# (Bags o),(LexOrder o) #) st S_{1}[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;

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

thus S_{1}[n,y]
; :: thesis: verum

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

then
support y = {n}
by PRE_POLY:def 7;( ( 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} ) )

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;

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

assume that 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;then x = n by TARSKI:def 1;

hence y . x <> 0 by A4, A5, FUNCT_7:31; :: thesis: verum

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;

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

thus S

A9: for n being Element of NAT holds S

reconsider f = f as sequence of RelStr(# (Bags o),(LexOrder o) #) ;

f is descending

proof

hence
contradiction
by A2, WELLFND1:14; :: thesis: verum
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;

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

then A19:
fn1 < fn
by A14, A16, PRE_POLY:def 9;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;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

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