let G be _finite _Graph; :: thesis: 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)))
let S be VNumberingSeq of G; :: thesis: 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)))
let i be Nat; :: thesis: 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)))
let a, b be set ; :: thesis: ( a in dom (S . i) & b in dom (S . i) & (S . i) . a < (S . i) . b implies b in dom (S . ((S .Lifespan()) -' ((S . i) . a))) )
assume that
A1: a in dom (S . i) and
A2: b in dom (S . i) and
A3: (S . i) . a < (S . i) . b ; :: thesis: b in dom (S . ((S .Lifespan()) -' ((S . i) . a)))
set GN = S .Lifespan() ;
set CSI = S . i;
set VLI = S . i;
set j = (S .Lifespan()) -' ((S . i) . a);
set CSJ = S . ((S .Lifespan()) -' ((S . i) . a));
set VLJ = S . ((S .Lifespan()) -' ((S . i) . a));
(S . i) . a <= S .Lifespan() by Th15;
then A4: (S .Lifespan()) -' ((S . i) . a) = (S .Lifespan()) - ((S . i) . a) by XREAL_1:233;
then (S .Lifespan()) -' ((S .Lifespan()) -' ((S . i) . a)) = (S .Lifespan()) - ((S .Lifespan()) - ((S . i) . a)) by NAT_D:35, XREAL_1:233;
then consider w being Vertex of G such that
A5: w in dom (S . ((S .Lifespan()) -' ((S . i) . a))) and
A6: (S . ((S .Lifespan()) -' ((S . i) . a))) . w = (S . i) . b by A3, Th15, Th16;

now :: thesis: not (S .Lifespan()) -' ((S . i) . a) >= i

assume (S .Lifespan()) -' ((S . i) . a) >= i ; :: thesis: contradiction
then S . i c= S . ((S .Lifespan()) -' ((S . i) . a)) by Th17;
then A7: dom (S . i) c= dom (S . ((S .Lifespan()) -' ((S . i) . a))) by RELAT_1:11;
0 < (S . i) . a by A1, Th15;
then A8: (S .Lifespan()) -' ((S . i) . a) < S .Lifespan() by A4, XREAL_1:44;
a = S .PickedAt ((S .Lifespan()) -' ((S . i) . a)) by A1, Th20;
hence contradiction by A1, A7, A8, Def9; :: thesis: verum

end;

then A9: S . ((S .Lifespan()) -' ((S . i) . a)) c= S . i by Th17;
A10: [w,((S . i) . b)] in S . ((S .Lifespan()) -' ((S . i) . a)) by A5, A6, FUNCT_1:1;
then A11: (S . i) . w = (S . i) . b by A9, FUNCT_1:1;
A12: S . i is one-to-one by Th18;
w in dom (S . i) by A9, A10, FUNCT_1:1;
hence b in dom (S . ((S .Lifespan()) -' ((S . i) . a))) by A2, A5, A11, A12, FUNCT_1:def 4; :: thesis: verum