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:235;
then A10: (G .order() ) -' j < G .order() by A7, XREAL_1:46;
A11: (G .order() ) - ((G .order() ) -' j) = (G .order() ) - ((G .order() ) - j) by A8, XREAL_1:235;
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:8;
then (G .order() ) + ((G .order() ) -' j) < (((G .order() ) + i) - ((G .order() ) -' j)) + ((G .order() ) -' j) by XREAL_1:8;
then A12: (((G .order() ) -' j) + (G .order() )) - (G .order() ) < (i + (G .order() )) - (G .order() ) by XREAL_1:11;
A13: w = ((LexBFS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' j) by A4, A7, A9, Th41, XREAL_1:46;
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 Def16;
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:235; :: thesis: verum