let G be _finite _Graph; for i, j being Nat
for v being Vertex of G st j in (((LexBFS:CSeq G) . i) `2) . v holds
ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )
let i, j be Nat; for v being Vertex of G st j in (((LexBFS:CSeq G) . i) `2) . v holds
ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )
let v be Vertex of G; ( j in (((LexBFS:CSeq G) . i) `2) . v implies ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} ) )
set CSI = (LexBFS:CSeq G) . i;
set VLI = ((LexBFS:CSeq G) ``1) . i;
set V2I = ((LexBFS:CSeq G) . i) `2 ;
set n = (G .order()) -' j;
set CSN = (LexBFS:CSeq G) . ((G .order()) -' j);
set VLN = ((LexBFS:CSeq G) . ((G .order()) -' j)) `1 ;
A1:
G .order() = (LexBFS:CSeq G) .Lifespan()
by Th37;
A2:
(LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1) .Lifespan()
by Th39;
assume A3:
j in (((LexBFS:CSeq G) . i) `2) . v
; ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )
then consider w being Vertex of G such that
A4:
LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order()) -' j)) = w
and
not w in dom (((LexBFS:CSeq G) . ((G .order()) -' j)) `1)
and
A5:
v in G .AdjacentSet {w}
by Th48;
A6:
(((LexBFS:CSeq G) . i) `2) . v c= (Seg (G .order())) \ (Seg ((G .order()) -' i))
by Th43;
then A7:
(G .order()) -' i < j
by A3, Th3;
A8:
j <= G .order()
by A3, A6, Th3;
then A9:
(G .order()) -' j = (G .order()) - j
by XREAL_1:233;
then A10:
(G .order()) -' j < G .order()
by A7, XREAL_1:44;
A11:
(G .order()) - ((G .order()) -' j) = (G .order()) - ((G .order()) - j)
by A8, XREAL_1:233;
then
(G .order()) - i < (G .order()) - ((G .order()) -' j)
by A7, XREAL_0:def 2;
then
((G .order()) - i) + i < ((G .order()) - ((G .order()) -' j)) + i
by XREAL_1:6;
then
(G .order()) + ((G .order()) -' j) < (((G .order()) + i) - ((G .order()) -' j)) + ((G .order()) -' j)
by XREAL_1:6;
then A12:
(((G .order()) -' j) + (G .order())) - (G .order()) < (i + (G .order())) - (G .order())
by XREAL_1:9;
A13:
w = ((LexBFS:CSeq G) ``1) .PickedAt ((G .order()) -' j)
by A4, A7, A9, Th41, XREAL_1:44;
then A14:
(((LexBFS:CSeq G) ``1) . i) . w = (G .order()) -' ((G .order()) -' j)
by A10, A1, A2, A12, Th21;
A15:
((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1) . i
by Def15;
then
w in dom (((LexBFS:CSeq G) . i) `1)
by A10, A1, A2, A13, A12, Th21;
hence
ex w being Vertex of G st
( w in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . w = j & v in G .AdjacentSet {w} )
by A15, A5, A10, A11, A14, XREAL_1:233; verum