let o be Ordinal; :: thesis: GrInvLexOrder o is well-ordering
set gilo = GrInvLexOrder o;
set ilo = InvLexOrder o;
A1:
GrInvLexOrder o is_strongly_connected_in Bags o
by Def7;
A2:
field (GrInvLexOrder o) = Bags o
by ORDERS_1:97;
then A3:
GrInvLexOrder o is_reflexive_in Bags o
by RELAT_2:def 9;
A4:
GrInvLexOrder o is_transitive_in Bags o
by A2, RELAT_2:def 16;
A5:
GrInvLexOrder o is_antisymmetric_in Bags o
by A2, RELAT_2:def 12;
A6:
GrInvLexOrder o is_connected_in field (GrInvLexOrder o)
by A1, A2, ORDERS_1:92;
A7:
for a, b, c being bag of st [a,b] in InvLexOrder o holds
[(a + c),(b + c)] in InvLexOrder o
by Def7;
now let Y be
set ;
:: thesis: ( Y c= field (GrInvLexOrder o) & Y <> {} implies ex a being set st
( a in Y & (GrInvLexOrder o) -Seg a misses Y ) )assume that A8:
Y c= field (GrInvLexOrder o)
and A9:
Y <> {}
;
:: thesis: ex a being set st
( a in Y & (GrInvLexOrder o) -Seg a misses Y )set TD =
{ (TotDegree y) where y is Element of Bags o : y in Y } ;
consider x being
set such that A10:
x in Y
by A9, XBOOLE_0:def 1;
reconsider x =
x as
Element of
Bags o by A8, A10, ORDERS_1:97;
A11:
TotDegree x in { (TotDegree y) where y is Element of Bags o : y in Y }
by A10;
{ (TotDegree y) where y is Element of Bags o : y in Y } c= NAT
then reconsider TD =
{ (TotDegree y) where y is Element of Bags o : y in Y } as non
empty Subset of
NAT by A11;
set mTD =
{ y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ;
A13:
{ y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } c= field (GrInvLexOrder o)
min TD in TD
by XXREAL_2:def 7;
then consider y being
Element of
Bags o such that A15:
TotDegree y = min TD
and A16:
y in Y
;
A17:
y in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) }
by A15, A16;
A18:
field (InvLexOrder o) = Bags o
by ORDERS_1:97;
InvLexOrder o is
well-ordering
by Th26;
then
InvLexOrder o well_orders field (InvLexOrder o)
by WELLORD1:8;
then
InvLexOrder o is_well_founded_in field (InvLexOrder o)
by WELLORD1:def 5;
then consider a being
set such that A19:
a in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) }
and A20:
(InvLexOrder o) -Seg a misses { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) }
by A2, A13, A17, A18, WELLORD1:def 3;
A21:
((InvLexOrder o) -Seg a) /\ { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } = {}
by A20, XBOOLE_0:def 7;
consider a' being
Element of
Bags o such that A22:
a' = a
and A23:
(
a' in Y &
TotDegree a' = min TD )
by A19;
take a =
a;
:: thesis: ( a in Y & (GrInvLexOrder o) -Seg a misses Y )thus
a in Y
by A22, A23;
:: thesis: (GrInvLexOrder o) -Seg a misses Yhence
(GrInvLexOrder o) -Seg a misses Y
by XBOOLE_0:def 7;
:: thesis: verum end;
then
GrInvLexOrder o is_well_founded_in field (GrInvLexOrder o)
by WELLORD1:def 3;
then
GrInvLexOrder o well_orders field (GrInvLexOrder o)
by A2, A3, A4, A5, A6, WELLORD1:def 5;
hence
GrInvLexOrder o is well-ordering
by WELLORD1:8; :: thesis: verum