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 ;
A0: ((LexBFS:CSeq G) . i) `1 = ((LexBFS:CSeq G) ``1 ) . i by d1stBFSLS;
assume A1: 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
A2: LexBFS:PickUnnumbered ((LexBFS:CSeq G) . ((G .order() ) -' j)) = w and
not w in dom (((LexBFS:CSeq G) . ((G .order() ) -' j)) `1 ) and
A3: v in G .AdjacentSet {w} by Th60;
(((LexBFS:CSeq G) . i) `2 ) . v c= (Seg (G .order() )) \ (Seg ((G .order() ) -' i)) by Th55;
then A4: ( (G .order() ) -' i < j & j <= G .order() ) by A1, Th5;
then A5: (G .order() ) -' j = (G .order() ) - j by XREAL_1:235;
then A6: (G .order() ) -' j < G .order() by A4, XREAL_1:46;
A7: (G .order() ) - ((G .order() ) -' j) = (G .order() ) - ((G .order() ) - j) by A4, XREAL_1:235;
A8: G .order() = (LexBFS:CSeq G) .Lifespan() by Th51;
A8a: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1 ) .Lifespan() by VNS0;
A9: w = ((LexBFS:CSeq G) ``1 ) .PickedAt ((G .order() ) -' j) by A2, A4, A5, Th53, XREAL_1:46;

now

(G .order() ) - i < (G .order() ) - ((G .order() ) -' j) by A4, 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 (((G .order() ) -' j) + (G .order() )) - (G .order() ) < (i + (G .order() )) - (G .order() ) by XREAL_1:11;
hence (G .order() ) -' j < i ; :: thesis: verum

end;

then ( w in dom (((LexBFS:CSeq G) . i) `1 ) & (((LexBFS:CSeq G) ``1 ) . i) . w = (G .order() ) -' ((G .order() ) -' j) ) by A0, A6, A8, A8a, A9, Th28;
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 A0, A3, A6, A7, XREAL_1:235; :: thesis: verum