let G be _finite _Graph; :: thesis: for n being Nat holds ((LexBFS:CSeq G) . n) `1 is with_property_L3
let i be Nat; :: thesis: ((LexBFS:CSeq G) . i) `1 is with_property_L3
set CSi = (LexBFS:CSeq G) . i;
set VLi = ((LexBFS:CSeq G) ``1) . i;
A1: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1) . i by Def15;

now :: thesis: for a, b, c being Vertex of G st a in dom (((LexBFS:CSeq G) ``1) . i) & b in dom (((LexBFS:CSeq G) ``1) . i) & c in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . b & (((LexBFS:CSeq G) ``1) . i) . b < (((LexBFS:CSeq G) ``1) . i) . c & a,c are_adjacent & not b,c are_adjacent holds
ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & b,d are_adjacent & not a,d are_adjacent & ( for e being Vertex of G st e <> d & e,b are_adjacent & not e,a are_adjacent holds
(((LexBFS:CSeq G) ``1) . i) . e < (((LexBFS:CSeq G) ``1) . i) . d ) )

A2: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1) .Lifespan() by Th39;
A3: (LexBFS:CSeq G) .Lifespan() = G .order() by Th37;
let a, b, c be Vertex of G; :: thesis: ( a in dom (((LexBFS:CSeq G) ``1) . i) & b in dom (((LexBFS:CSeq G) ``1) . i) & c in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . b & (((LexBFS:CSeq G) ``1) . i) . b < (((LexBFS:CSeq G) ``1) . i) . c & a,c are_adjacent & not b,c are_adjacent implies ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & b,d are_adjacent & not a,d are_adjacent & ( for e being Vertex of G st e <> d & e,b are_adjacent & not e,a are_adjacent holds
(((LexBFS:CSeq G) ``1) . i) . e < (((LexBFS:CSeq G) ``1) . i) . d ) ) )
assume that
A4: a in dom (((LexBFS:CSeq G) ``1) . i) and
A5: b in dom (((LexBFS:CSeq G) ``1) . i) and
A6: c in dom (((LexBFS:CSeq G) ``1) . i) and
A7: (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . b and
A8: (((LexBFS:CSeq G) ``1) . i) . b < (((LexBFS:CSeq G) ``1) . i) . c and
A9: a,c are_adjacent and
A10: not b,c are_adjacent ; :: thesis: ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & b,d are_adjacent & not a,d are_adjacent & ( for e being Vertex of G st e <> d & e,b are_adjacent & not e,a are_adjacent holds
(((LexBFS:CSeq G) ``1) . i) . e < (((LexBFS:CSeq G) ``1) . i) . d ) )
defpred S<sub>1</sub>[ Nat] means ex v being Vertex of G st
( v in dom (((LexBFS:CSeq G) ``1) . i) & b,v are_adjacent & not a,v are_adjacent & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . v & (((LexBFS:CSeq G) ``1) . i) . v = $1 );
A11: (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . c by A7, A8, XXREAL_0:2;

now :: thesis: ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & d,b are_adjacent & not d,a are_adjacent )

set kc = (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c);
set k = (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b);
assume A12: for d being Vertex of G st d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & d,b are_adjacent holds
d,a are_adjacent ; :: thesis: contradiction
set VLc = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c));
set CSc = (LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c));
set VLb = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b));
set CSb = (LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b));
reconsider sb = (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `2) . b, sa = (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `2) . a as finite Subset of NAT ;
A13: (Seg (G .order())) \ (Seg ((G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b)))) c= Seg (G .order()) by XBOOLE_1:36;
sb c= (Seg (G .order())) \ (Seg ((G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b)))) by Th43;
then A14: sb c= Seg (G .order()) by A13;
A15: ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) `1 = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c)) by Def15;
sa c= (Seg (G .order())) \ (Seg ((G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b)))) by Th43;
then A16: sa c= Seg (G .order()) by A13;
A17: c in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) by A5, A6, A8, A3, A2, Th23;
A18: (((LexBFS:CSeq G) ``1) . i) . c <= G .order() by A3, A2, Th15;
then A19: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c) = (G .order()) - ((((LexBFS:CSeq G) ``1) . i) . c) by XREAL_1:233;
then A20: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c) < G .order() by A8, XREAL_1:44;
then A21: (G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c)) = (G .order()) - ((G .order()) - ((((LexBFS:CSeq G) ``1) . i) . c)) by A19, XREAL_1:233;

A22: now :: thesis: not a in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c)))

A23: rng (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) = (Seg (G .order())) \ (Seg ((G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c)))) by A3, A2, Th14;
A24: (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . c by A7, A8, XXREAL_0:2;
assume A25: a in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) ; :: thesis: contradiction
then (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) . a in rng (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) by FUNCT_1:def 3;
then (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) . a by A21, A23, Th3;
hence contradiction by A4, A25, A24, Th19; :: thesis: verum

end;

((LexBFS:CSeq G) ``1) .PickedAt ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c)) = c by A6, A3, A2, Th20;
then A26: c = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c))) by A8, A19, Th41, XREAL_1:44;
A27: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . c) < (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b) by A8, A18, Th2;
set j = (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c;
A28: ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1 = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b)) by Def15;
a in G .AdjacentSet {c} by A7, A8, A9, CHORD:52;
then (((LexBFS:CSeq G) ``1) . i) . c in sa by A15, A20, A27, A26, A21, A22, Th45;
then A29: (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in sa by A6, A17, Th19;
A30: not b in G .AdjacentSet {c} by A10, CHORD:52;

A31: now :: thesis: not (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in sb

assume (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in sb ; :: thesis: contradiction
then A32: ex z being Vertex of G st
( z in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) & (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . z = (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c & b in G .AdjacentSet {z} ) by A28, Th52;
((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b)) is one-to-one by Th18;
hence contradiction by A30, A17, A32, FUNCT_1:def 4; :: thesis: verum

end;

then ((sb,1) -bag) . ((((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c) = 0 by UPROOTS:6;
then A33: ((sb,1) -bag) . ((((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c) < ((sa,1) -bag) . ((((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c) by A29, UPROOTS:7;
[((sb,1) -bag),((sa,1) -bag)] in InvLexOrder NAT

proof

per cases ( for k being Ordinal st (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in k & k in NAT holds
((sb,1) -bag) . k = ((sa,1) -bag) . k or ex k being Ordinal st
( (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in k & k in NAT & not ((sb,1) -bag) . k = ((sa,1) -bag) . k ) ) ;

suppose for k being Ordinal st (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in k & k in NAT holds
((sb,1) -bag) . k = ((sa,1) -bag) . k ; :: thesis: [((sb,1) -bag),((sa,1) -bag)] in InvLexOrder NAT

hence [((sb,1) -bag),((sa,1) -bag)] in InvLexOrder NAT by A33, BAGORDER:def 6; :: thesis: verum

end;

suppose A34: ex k being Ordinal st
( (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in k & k in NAT & not ((sb,1) -bag) . k = ((sa,1) -bag) . k ) ; :: thesis: [((sb,1) -bag),((sa,1) -bag)] in InvLexOrder NAT

defpred S₂[ Nat] means ( (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in $1 & ((sb,1) -bag) . $1 <> ((sa,1) -bag) . $1 );
A35: for k being Nat st S₂[k] holds
k <= G .order()

proof

let k be Nat; :: thesis: ( S₂[k] implies k <= G .order() )
assume A36: S₂[k] ; :: thesis: k <= G .order()
A37: ( ((sa,1) -bag) . k = 1 or ((sa,1) -bag) . k = 0 ) by UPROOTS:6, UPROOTS:7;
k in NAT by ORDINAL1:def 12;
then consider ok being Ordinal such that
A38: ok = k and
(((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in ok and
ok in NAT and
A39: ((sb,1) -bag) . ok <> ((sa,1) -bag) . ok by A36;

per cases ( not ok in sb or ok in sb ) ;

suppose not ok in sb ; :: thesis: k <= G .order()

then ok in sa by A38, A39, A37, UPROOTS:6;
hence k <= G .order() by A16, A38, FINSEQ_1:1; :: thesis: verum

end;

suppose ok in sb ; :: thesis: k <= G .order()

hence k <= G .order() by A14, A38, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

A40: ex k being Nat st S₂[k] by A34;
consider mm being Nat such that
A41: S₂[mm] and
A42: for i being Nat st S₂[i] holds
i <= mm from NAT_1:sch 6(A35, A40);
reconsider mm = mm as Element of NAT by ORDINAL1:def 12;

A43: now :: thesis: for k being Ordinal st mm in k & k in NAT holds
not ((sb,1) -bag) . k <> ((sa,1) -bag) . k

let k be Ordinal; :: thesis: ( mm in k & k in NAT implies not ((sb,1) -bag) . k <> ((sa,1) -bag) . k )
assume that
A44: mm in k and
A45: k in NAT ; :: thesis: not ((sb,1) -bag) . k <> ((sa,1) -bag) . k
reconsider kk = k as Element of NAT by A45;
mm in { y where y is Nat : y < kk } by A44, AXIOMS:4;
then A46: ex mmy being Nat st
( mmy = mm & mmy < kk ) ;
assume ((sb,1) -bag) . k <> ((sa,1) -bag) . k ; :: thesis: contradiction
hence contradiction by A41, A42, A44, A46, ORDINAL1:10; :: thesis: verum

end;

(((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c in { y where y is Nat : y < mm } by A41, AXIOMS:4;
then A47: ex jy being Nat st
( jy = (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c & jy < mm ) ;

A48: now :: thesis: not ((sb,1) -bag) . mm = 1

assume A49: ((sb,1) -bag) . mm = 1 ; :: thesis: contradiction
then mm in sb by UPROOTS:6;
then consider z being Vertex of G such that
A50: z in dom (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1) and
A51: (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1) . z = mm and
A52: b in G .AdjacentSet {z} by Th52;
set kc = (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z);
A53: (((LexBFS:CSeq G) ``1) . i) . z <= G .order() by A3, A2, Th15;
then A54: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z) = (G .order()) - ((((LexBFS:CSeq G) ``1) . i) . z) by XREAL_1:233;
(G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b) < i by A5, A3, A2, Th22;
then A55: ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1 c= ((LexBFS:CSeq G) . i) `1 by A1, A28, Th17;
then A56: dom (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1) c= dom (((LexBFS:CSeq G) . i) `1) by RELAT_1:11;
then A57: 0 < (((LexBFS:CSeq G) ``1) . i) . z by A1, A50, Th15;
then A58: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z) < G .order() by A54, XREAL_1:44;
then A59: (G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)) = (G .order()) - ((G .order()) - ((((LexBFS:CSeq G) ``1) . i) . z)) by A54, XREAL_1:233;
set VLc = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z));
set CSc = (LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z));
z = ((LexBFS:CSeq G) ``1) .PickedAt ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)) by A1, A3, A2, A50, A56, Th20;
then A60: z = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) by A57, A54, Th41, XREAL_1:44;
A61: [z,mm] in ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1 by A50, A51, FUNCT_1:def 2;
then A62: (((LexBFS:CSeq G) ``1) . i) . z = mm by A1, A50, A55, A56, FUNCT_1:def 2;
A63: [c,((((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c)] in ((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `1 by A28, A17, FUNCT_1:def 2;
then A64: (((LexBFS:CSeq G) ``1) . i) . c = (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) . c by A1, A6, A55, FUNCT_1:def 2;
then (((LexBFS:CSeq G) ``1) . i) . b < (((LexBFS:CSeq G) ``1) . i) . z by A8, A47, A62, XXREAL_0:2;
then A65: (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z) < (G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b) by A53, Th2;
A66: (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . z by A1, A47, A50, A55, A56, A61, A64, FUNCT_1:def 2;

A67: now :: thesis: not a in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)))

(((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . c by A7, A8, XXREAL_0:2;
then A68: (((LexBFS:CSeq G) ``1) . i) . a < (((LexBFS:CSeq G) ``1) . i) . z by A66, XXREAL_0:2;
A69: rng (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) = (Seg (G .order())) \ (Seg ((G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)))) by A3, A2, Th14;
assume A70: a in dom (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) ; :: thesis: contradiction
then (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) . a in rng (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) by FUNCT_1:def 3;
then (((LexBFS:CSeq G) ``1) . i) . z < (((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) . a by A59, A69, Th3;
hence contradiction by A4, A70, A68, Th19; :: thesis: verum

end;

A71: (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . z by A1, A6, A47, A55, A62, A63, FUNCT_1:def 2;
b,z are_adjacent by A52, CHORD:52;
then z,a are_adjacent by A1, A12, A47, A50, A56, A62, A64;
then A72: a in G .AdjacentSet {z} by A11, A71, CHORD:52;
((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z))) `1 = ((LexBFS:CSeq G) ``1) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)) by Def15;
then (G .order()) -' ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . z)) in (((LexBFS:CSeq G) . ((G .order()) -' ((((LexBFS:CSeq G) ``1) . i) . b))) `2) . a by A72, A58, A65, A60, A67, Th45;
hence contradiction by A41, A49, A62, A59, UPROOTS:7; :: thesis: verum

end;

( ((sb,1) -bag) . mm = 0 or ((sb,1) -bag) . mm = 1 ) by UPROOTS:6, UPROOTS:7;
hence [((sb,1) -bag),((sa,1) -bag)] in InvLexOrder NAT by A41, A48, A43, BAGORDER:def 6; :: thesis: verum

end;

end;

end;

then A73: (sb,1) -bag <= (sa,1) -bag , InvLexOrder NAT by TERMORD:def 2;
(sb,1) -bag <> (sa,1) -bag by A29, A31, Th6;
then A74: (sb,1) -bag < (sa,1) -bag , InvLexOrder NAT by A73, TERMORD:def 3;
(sa,1) -bag <= (sb,1) -bag , InvLexOrder NAT by A1, A4, A5, A7, Th51;
hence contradiction by A74, TERMORD:5; :: thesis: verum

end;

then A75: ex k being Nat st S₁[k] ;
A76: for k being Nat st S₁[k] holds
k <= G .order()

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= G .order() )
assume S₁[k] ; :: thesis: k <= G .order()
then k in rng (((LexBFS:CSeq G) ``1) . i) by FUNCT_1:def 3;
then A77: k in (Seg (G .order())) \ (Seg ((G .order()) -' i)) by A3, A2, Th14;
(Seg (G .order())) \ (Seg ((G .order()) -' i)) c= Seg (G .order()) by XBOOLE_1:36;
hence k <= G .order() by A77, FINSEQ_1:1; :: thesis: verum

end;

ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A76, A75);
then consider k being Nat such that
A78: S₁[k] and
A79: for n being Nat st S₁[n] holds
n <= k ;
consider v being Vertex of G such that
A80: v in dom (((LexBFS:CSeq G) ``1) . i) and
A81: b,v are_adjacent and
A82: not a,v are_adjacent and
A83: (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . v and
A84: (((LexBFS:CSeq G) ``1) . i) . v = k by A78;
for d being Vertex of G st d <> v & d,b are_adjacent & not d,a are_adjacent holds
(((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v

proof

let d be Vertex of G; :: thesis: ( d <> v & d,b are_adjacent & not d,a are_adjacent implies (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v )
assume that
A85: d <> v and
A86: d,b are_adjacent and
A87: not d,a are_adjacent ; :: thesis: (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v

per cases ( (((LexBFS:CSeq G) ``1) . i) . d <= (((LexBFS:CSeq G) ``1) . i) . c or (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d ) ;

suppose (((LexBFS:CSeq G) ``1) . i) . d <= (((LexBFS:CSeq G) ``1) . i) . c ; :: thesis: (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v

hence (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v by A83, XXREAL_0:2; :: thesis: verum

end;

suppose A88: (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d ; :: thesis: (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v

then A89: d in dom (((LexBFS:CSeq G) ``1) . i) by FUNCT_1:def 2;
((LexBFS:CSeq G) ``1) . i is one-to-one by Th18;
then A90: (((LexBFS:CSeq G) ``1) . i) . d <> (((LexBFS:CSeq G) ``1) . i) . v by A80, A85, A89, FUNCT_1:def 4;
(((LexBFS:CSeq G) ``1) . i) . d <= k by A79, A86, A87, A88, A89;
hence (((LexBFS:CSeq G) ``1) . i) . d < (((LexBFS:CSeq G) ``1) . i) . v by A84, A90, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ex d being Vertex of G st
( d in dom (((LexBFS:CSeq G) ``1) . i) & (((LexBFS:CSeq G) ``1) . i) . c < (((LexBFS:CSeq G) ``1) . i) . d & b,d are_adjacent & not a,d are_adjacent & ( for e being Vertex of G st e <> d & e,b are_adjacent & not e,a are_adjacent holds
(((LexBFS:CSeq G) ``1) . i) . e < (((LexBFS:CSeq G) ``1) . i) . d ) ) by A80, A81, A82, A83; :: thesis: verum

end;

hence ((LexBFS:CSeq G) . i) `1 is with_property_L3 by A1; :: thesis: verum