theorem Th24: :: LEXBFS:24

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) & (S . i) . a < (S . i) . b holds
not a in dom (S . ((S .Lifespan()) -' ((S . i) . b)))