theorem Th42: :: LEXBFS:42

for G being _finite _Graph
for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((LexBFS:CSeq G) . n) `1) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = ((((LexBFS:CSeq G) . n) `2) . v) \/ {((G .order()) -' n)} ) & ( ( not v in G .AdjacentSet {w} or v in dom (((LexBFS:CSeq G) . n) `1) ) implies (((LexBFS:CSeq G) . (n + 1)) `2) . v = (((LexBFS:CSeq G) . n) `2) . v ) ) ) )