theorem Th22: :: LEXBFS:22

for G being finite _Graph
for S being VNumberingSeq of G
for m being Nat
for v being set st v in dom (S . m) holds
( (S .Lifespan()) -' ((S . m) . v) < m & (S .Lifespan()) -' m < (S . m) . v )