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 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));
set GN = S .Lifespan() ;
(S . i) . a <= S .Lifespan() by Th22;
then A4: (S .Lifespan() ) -' ((S . i) . a) = (S .Lifespan() ) - ((S . i) . a) by XREAL_1:235;
then (S .Lifespan() ) -' ((S .Lifespan() ) -' ((S . i) . a)) = (S .Lifespan() ) - ((S .Lifespan() ) - ((S . i) . a)) by XREAL_1:235, NAT_D:35;
then consider w being Vertex of G such that
A6: w in dom (S . ((S .Lifespan() ) -' ((S . i) . a))) and
A7: (S . ((S .Lifespan() ) -' ((S . i) . a))) . w = (S . i) . b by A3, Th22, Th23;

now

assume (S .Lifespan() ) -' ((S . i) . a) >= i ; :: thesis: contradiction
then S . i c= S . ((S .Lifespan() ) -' ((S . i) . a)) by Th24;
then A8: dom (S . i) c= dom (S . ((S .Lifespan() ) -' ((S . i) . a))) by RELAT_1:25;
A9: a = S .PickedAt ((S .Lifespan() ) -' ((S . i) . a)) by A1, Th27;
0 < (S . i) . a by A1, Th22;
then (S .Lifespan() ) -' ((S . i) . a) < S .Lifespan() by A4, XREAL_1:46;
hence contradiction by A1, A8, A9, Def27; :: thesis: verum

end;

then A10: S . ((S .Lifespan() ) -' ((S . i) . a)) c= S . i by Th24;
[w,((S . i) . b)] in S . ((S .Lifespan() ) -' ((S . i) . a)) by A6, A7, FUNCT_1:8;
then A11: ( w in dom (S . i) & (S . i) . w = (S . i) . b ) by A10, FUNCT_1:8;
S . i is one-to-one by Th25;
hence b in dom (S . ((S .Lifespan() ) -' ((S . i) . a))) by A2, A6, A11, FUNCT_1:def 8; :: thesis: verum