:: deftheorem Def9 defines .PickedAt LEXBFS:def 10 :
for G being _finite _Graph
for S being VNumberingSeq of G
for n being Nat
for b₄ being set holds
( ( n >= S .Lifespan() implies ( b₄ = S .PickedAt n iff b₄ = the Element of the_Vertices_of G ) ) & ( not n >= S .Lifespan() implies ( b₄ = S .PickedAt n iff ( not b₄ in dom (S . n) & S . (n + 1) = (S . n) +* (b₄ .--> ((S .Lifespan()) -' n)) ) ) ) );