let o be infinite Ordinal; 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
; 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 S1[ set , set ] means $2 = (o --> 0) +* ($1,1);
consider f being sequence of the carrier of RelStr(# (Bags o),(LexOrder o) #) such that
A9:
for n being Element of NAT holds S1[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;
WELLFND1:def 6 ( 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;
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;
[(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;
verum
end;
hence
contradiction
by A2, WELLFND1:14; verum