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 Def5;
A2: field (GrInvLexOrder o) = Bags o by ORDERS_1:12;
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;
A7: for a, b, c being bag of o st [a,b] in InvLexOrder o holds
[(a + c),(b + c)] in InvLexOrder o by Def5;

now :: thesis: for Y being set st Y c= field (GrInvLexOrder o) & Y <> {} holds
ex a being object st
( a in Y & (GrInvLexOrder o) -Seg a misses Y )

let Y be set ; :: thesis: ( Y c= field (GrInvLexOrder o) & Y <> {} implies ex a being object 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 object 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 object 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:12;
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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (TotDegree y) where y is Element of Bags o : y in Y } or x in NAT )
assume x in { (TotDegree y) where y is Element of Bags o : y in Y } ; :: thesis: x in NAT
then ex y being Element of Bags o st
( x = TotDegree y & y in Y ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

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 ) } ;
A12: { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } c= field (GrInvLexOrder o)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } or x in field (GrInvLexOrder o) )
assume x in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ; :: thesis: x in field (GrInvLexOrder o)
then ex y being Element of Bags o st
( x = y & y in Y & TotDegree y = min TD ) ;
hence x in field (GrInvLexOrder o) by A2; :: thesis: verum

end;

min TD in TD by XXREAL_2:def 7;
then consider y being Element of Bags o such that
A13: TotDegree y = min TD and
A14: y in Y ;
A15: y in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A13, A14;
A16: field (InvLexOrder o) = Bags o by ORDERS_1:12;
InvLexOrder o is well-ordering by Th22;
then InvLexOrder o well_orders field (InvLexOrder o) by WELLORD1:4;
then InvLexOrder o is_well_founded_in field (InvLexOrder o) by WELLORD1:def 5;
then consider a being object such that
A17: a in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } and
A18: (InvLexOrder o) -Seg a misses { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A2, A12, A15, A16, WELLORD1:def 3;
A19: ((InvLexOrder o) -Seg a) /\ { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } = {} by A18, XBOOLE_0:def 7;
A20: ex a9 being Element of Bags o st
( a9 = a & a9 in Y & TotDegree a9 = min TD ) by A17;
take a = a; :: thesis: ( a in Y & (GrInvLexOrder o) -Seg a misses Y )
thus a in Y by A20; :: thesis: (GrInvLexOrder o) -Seg a misses Y

now :: thesis: not ((GrInvLexOrder o) -Seg a) /\ Y <> {}

assume ((GrInvLexOrder o) -Seg a) /\ Y <> {} ; :: thesis: contradiction
then consider z being object such that
A21: z in ((GrInvLexOrder o) -Seg a) /\ Y by XBOOLE_0:def 1;
A22: z in (GrInvLexOrder o) -Seg a by A21, XBOOLE_0:def 4;
A23: z in Y by A21, XBOOLE_0:def 4;
A24: z <> a by A22, WELLORD1:1;
A25: [z,a] in GrInvLexOrder o by A22, WELLORD1:1;
reconsider a = a, z = z as Element of Bags o by A8, A20, A23, ORDERS_1:12;

per cases ( TotDegree z < TotDegree a or TotDegree z = TotDegree a or TotDegree z > TotDegree a ) by XXREAL_0:1;

suppose A26: TotDegree z < TotDegree a ; :: thesis: contradiction

TotDegree z in TD by A23;
hence contradiction by A20, A26, XXREAL_2:def 7; :: thesis: verum

end;

suppose A27: TotDegree z = TotDegree a ; :: thesis: contradiction

then [z,a] in InvLexOrder o by A7, A25, Def7;
then A28: z in (InvLexOrder o) -Seg a by A24, WELLORD1:1;
z in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A20, A23, A27;
hence contradiction by A19, A28, XBOOLE_0:def 4; :: thesis: verum

end;

suppose TotDegree z > TotDegree a ; :: thesis: contradiction

hence contradiction by A7, A25, Def7; :: thesis: verum

end;

end;

end;

hence (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:4; :: thesis: verum