let G be _finite _Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum