:: deftheorem Def8 defines vertex-numbering LEXBFS:def 9 :
for G being _finite _Graph
for S being preVNumberingSeq of G holds
( S is vertex-numbering iff ( S . 0 = {} & S is iterative & S is halting & S .Lifespan() = G .order() & ( for n being Nat st n < S .Lifespan() holds
ex w being Vertex of G st
( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) ) ) );