theorem Th23: :: LEXBFS:23

for G being _finite _Graph
for S being VNumberingSeq of G
for i being Nat
for a, b being set st a in dom (S . i) & b in dom (S . i) & (S . i) . a < (S . i) . b holds
b in dom (S . ((S .Lifespan()) -' ((S . i) . a)))