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;
i0: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1 ) . i by d1stBFSLS;

now

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 A1: ( 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 ) ; :: 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 ) )
A3: (LexBFS:CSeq G) .Lifespan() = G .order() by Th51;
A3a: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1 ) .Lifespan() by VNS0;
A5: (((LexBFS:CSeq G) ``1 ) . i) . a < (((LexBFS:CSeq G) ``1 ) . i) . c by A1, XXREAL_0:2;

now

assume A6: 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 k = (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b);
set CSb = (LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b));
set VLb = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b));
b0: ((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 d1stBFSLS;
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 ;
A9: (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 Th55;
then A10: sb c= Seg (G .order() ) by A9, XBOOLE_1:1;
sa c= (Seg (G .order() )) \ (Seg ((G .order() ) -' ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b)))) by Th55;
then A11: sa c= Seg (G .order() ) by A9, XBOOLE_1:1;
A13: not b in G .AdjacentSet {c} by A1, CHORD:52;
A14: a in G .AdjacentSet {c} by A1, CHORD:52;
A16: c in dom (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) by A1, A3, A3a, Th30;
set kc = (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c);
set CSc = (LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c));
set VLc = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c));
c0: ((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 d1stBFSLS;
A17: ( 1 <= (((LexBFS:CSeq G) ``1 ) . i) . c & (((LexBFS:CSeq G) ``1 ) . i) . c <= G .order() ) by A3, A3a, A1, Th22;
then A18: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c) = (G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . c) by XREAL_1:235;
then A19: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c) < G .order() by A1, XREAL_1:46;
A20: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c) < (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b) by A1, A17, Th2;
((LexBFS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c)) = c by A1, A3, A3a, Th27;
then A21: c = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c))) by A1, A18, Th53, XREAL_1:46;
A22: (G .order() ) -' ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c)) = (G .order() ) - ((G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . c)) by A18, A19, XREAL_1:235;

now

assume A23: a in dom (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c))) ; :: thesis: contradiction
then A24: (((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 5;
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, A3a, Th21;
then A25: (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c))) . a by A22, A24, Th5;
( a in dom (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . c))) & a in dom (((LexBFS:CSeq G) ``1 ) . i) & (((LexBFS:CSeq G) ``1 ) . i) . a < (((LexBFS:CSeq G) ``1 ) . i) . c ) by A1, A23, XXREAL_0:2;
hence contradiction by A25, Th26; :: thesis: verum

end;

then (((LexBFS:CSeq G) ``1 ) . i) . c in sa by c0, A14, A19, A20, A21, A22, Th57;
then A26: (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c in sa by A1, A16, Th26;

A27: now

assume (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c in sb ; :: thesis: contradiction
then consider z being Vertex of G such that
A28: z in dom (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) and
A29: (((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 and
A30: b in G .AdjacentSet {z} by b0, Th64;
((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b)) is one-to-one by Th25;
hence contradiction by A13, A16, A28, A29, A30, FUNCT_1:def 8; :: thesis: verum

end;

then A31: sb,1 -bag <> sa,1 -bag by A26, Th8;
A32: sa,1 -bag <= sb,1 -bag , InvLexOrder NAT by i0, A1, Th63;
set j = (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c;
(sb,1 -bag ) . ((((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c) = 0 by A27, UPROOTS:8;
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 A26, UPROOTS:9;
[(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 8; :: thesis: verum

end;

suppose 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

then consider qq being Ordinal such that
A34: ( (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c in qq & qq in NAT ) and
A35: (sb,1 -bag ) . qq <> (sa,1 -bag ) . qq ;
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 );
A36: ex k being Nat st S₁[k] by A34, A35;
A37: for k being Nat st S₁[k] holds
k <= G .order()

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= G .order() )
assume A38: S₁[k] ; :: thesis: k <= G .order()
k in NAT by ORDINAL1:def 13;
then consider ok being Ordinal such that
A39: ok = k and
( (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c in ok & ok in NAT ) and
A40: (sb,1 -bag ) . ok <> (sa,1 -bag ) . ok by A38;
A41: ( (sa,1 -bag ) . k = 1 or (sa,1 -bag ) . k = 0 ) by UPROOTS:8, UPROOTS:9;

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

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

then ok in sa by A39, A40, A41, UPROOTS:8;
hence k <= G .order() by A11, A39, FINSEQ_1:3; :: thesis: verum

end;

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

hence k <= G .order() by A10, A39, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

consider mm being Nat such that
A42: S₁[mm] and
A43: for i being Nat st S₁[i] holds
i <= mm from NAT_1:sch 6(A37, A36);
reconsider mm = mm as Element of NAT by ORDINAL1:def 13;
(((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c in { y where y is Element of NAT : y < mm } by A42, AXIOMS:30;
then consider jy being Element of NAT such that
A44: ( jy = (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c & jy < mm ) ;
A45: ( (sb,1 -bag ) . mm = 0 or (sb,1 -bag ) . mm = 1 ) by UPROOTS:8, UPROOTS:9;

Aaux: now

assume A46: (sb,1 -bag ) . mm = 1 ; :: thesis: contradiction
then mm in sb by UPROOTS:8;
then consider z being Vertex of G such that
A47: z in dom (((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) `1 ) and
A48: (((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) `1 ) . z = mm and
A49: b in G .AdjacentSet {z} by Th64;
(G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b) < i by A3, A3a, A1, Th29;
then A50: ((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) `1 c= ((LexBFS:CSeq G) . i) `1 by i0, b0, Th24;
then A51: dom (((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) `1 ) c= dom (((LexBFS:CSeq G) . i) `1 ) by RELAT_1:25;
A52: [z,mm] in ((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) `1 by A47, A48, FUNCT_1:def 4;
then A53: (((LexBFS:CSeq G) ``1 ) . i) . z = mm by i0, A47, A50, A51, FUNCT_1:def 4;
A54: [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 b0, A16, FUNCT_1:def 4;
then A55: (((LexBFS:CSeq G) ``1 ) . i) . c = (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b))) . c by i0, A1, A50, FUNCT_1:def 4;
A56: (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . i) . z by i0, A1, A44, A50, A53, A54, FUNCT_1:def 4;
b,z are_adjacent by A49, CHORD:52;
then z,a are_adjacent by i0, A6, A44, A47, A51, A53, A55;
then A57: a in G .AdjacentSet {z} by A5, A56, CHORD:52;
set kc = (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z);
set CSc = (LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z));
set VLc = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z));
c0: ((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 d1stBFSLS;
A58: (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . i) . z by i0, A44, A47, A50, A51, A52, A55, FUNCT_1:def 4;
A59: (((LexBFS:CSeq G) ``1 ) . i) . b < (((LexBFS:CSeq G) ``1 ) . i) . z by A1, A44, A53, A55, XXREAL_0:2;
A61: ( 1 <= (((LexBFS:CSeq G) ``1 ) . i) . z & (((LexBFS:CSeq G) ``1 ) . i) . z <= G .order() ) by A47, A51, i0, A3, A3a, Th22;
A62: 0 < (((LexBFS:CSeq G) ``1 ) . i) . z by i0, A47, A51, Th22;
A63: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z) = (G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . z) by A61, XREAL_1:235;
then A64: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z) < G .order() by A62, XREAL_1:46;
A65: (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z) < (G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . b) by A59, A61, Th2;
z = ((LexBFS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z)) by i0, A3, A3a, A47, A51, Th27;
then A66: z = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z))) by A62, A63, Th53, XREAL_1:46;
A67: (G .order() ) -' ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z)) = (G .order() ) - ((G .order() ) - ((((LexBFS:CSeq G) ``1 ) . i) . z)) by A63, A64, XREAL_1:235;

now

assume A68: a in dom (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z))) ; :: thesis: contradiction
then A69: (((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 5;
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, A3a, Th21;
then A70: (((LexBFS:CSeq G) ``1 ) . i) . z < (((LexBFS:CSeq G) ``1 ) . ((G .order() ) -' ((((LexBFS:CSeq G) ``1 ) . i) . z))) . a by A67, A69, Th5;
( a in dom (((LexBFS:CSeq G) ``1 ) . i) & (((LexBFS:CSeq G) ``1 ) . i) . a < (((LexBFS:CSeq G) ``1 ) . i) . c ) by A1, XXREAL_0:2;
then A71: (((LexBFS:CSeq G) ``1 ) . i) . a < (((LexBFS:CSeq G) ``1 ) . i) . z by A58, XXREAL_0:2;
thus contradiction by A1, A68, A70, A71, Th26; :: thesis: verum

end;

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 c0, A57, A64, A65, A66, Th57;
hence contradiction by A42, A46, A53, A67, UPROOTS:9; :: thesis: verum

end;

now

let k be Ordinal; :: thesis: ( mm in k & k in NAT implies not (sb,1 -bag ) . k <> (sa,1 -bag ) . k )
assume A73: ( mm in k & k in NAT ) ; :: thesis: not (sb,1 -bag ) . k <> (sa,1 -bag ) . k
reconsider kk = k as Element of NAT by A73;
assume A74: (sb,1 -bag ) . k <> (sa,1 -bag ) . k ; :: thesis: contradiction
mm in { y where y is Element of NAT : y < kk } by A73, AXIOMS:30;
then consider mmy being Element of NAT such that
A75: ( mmy = mm & mmy < kk ) ;
thus contradiction by A42, A43, A73, A74, A75, ORDINAL1:19; :: thesis: verum

end;

hence [(sb,1 -bag ),(sa,1 -bag )] in InvLexOrder NAT by Aaux, A42, A45, BAGORDER:def 8; :: thesis: verum

end;

end;

end;

then sb,1 -bag <= sa,1 -bag , InvLexOrder NAT by TERMORD:def 2;
then sb,1 -bag < sa,1 -bag , InvLexOrder NAT by A31, TERMORD:def 3;
hence contradiction by A32, TERMORD:5; :: thesis: verum

end;

then consider x being Vertex of G such that
A76: ( x in dom (((LexBFS:CSeq G) ``1 ) . i) & (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . i) . x & x,b are_adjacent & not x,a are_adjacent ) ;
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 );
A77: ex k being Nat st S₁[k] by A76;
A78: for k being Nat st S₁[k] holds
k <= G .order()

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= G .order() )
assume A79: S₁[k] ; :: thesis: k <= G .order()
consider v being Vertex of G such that
A80: ( v in dom (((LexBFS:CSeq G) ``1 ) . i) & v,b are_adjacent & not v,a are_adjacent ) and
A81: ( (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . i) . v & (((LexBFS:CSeq G) ``1 ) . i) . v = k ) by A79;
k in rng (((LexBFS:CSeq G) ``1 ) . i) by A80, A81, FUNCT_1:def 5;
then A82: k in (Seg (G .order() )) \ (Seg ((G .order() ) -' i)) by A3, A3a, Th21;
(Seg (G .order() )) \ (Seg ((G .order() ) -' i)) c= Seg (G .order() ) by XBOOLE_1:36;
hence k <= G .order() by A82, FINSEQ_1:3; :: 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(A78, A77);
then consider k being Nat such that
A83: S₁[k] and
A84: for n being Nat st S₁[n] holds
n <= k ;
consider v being Vertex of G such that
A85: ( v in dom (((LexBFS:CSeq G) ``1 ) . i) & b,v are_adjacent & not a,v are_adjacent ) and
A86: (((LexBFS:CSeq G) ``1 ) . i) . c < (((LexBFS:CSeq G) ``1 ) . i) . v and
A87: (((LexBFS:CSeq G) ``1 ) . i) . v = k by A83;
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 A88: ( d <> v & d,b are_adjacent & 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 A86, XXREAL_0:2; :: thesis: verum

end;

suppose A89: (((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 A90: d in dom (((LexBFS:CSeq G) ``1 ) . i) by FUNCT_1:def 4;
then A91: (((LexBFS:CSeq G) ``1 ) . i) . d <= k by A84, A88, A89;
((LexBFS:CSeq G) ``1 ) . i is one-to-one by Th25;
then (((LexBFS:CSeq G) ``1 ) . i) . d <> (((LexBFS:CSeq G) ``1 ) . i) . v by A85, A88, A90, FUNCT_1:def 8;
hence (((LexBFS:CSeq G) ``1 ) . i) . d < (((LexBFS:CSeq G) ``1 ) . i) . v by A87, A91, 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 A85, A86; :: thesis: verum

end;

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