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
not a in dom (S . ((S .Lifespan() ) -' ((S . i) . b)))
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
not a in dom (S . ((S .Lifespan() ) -' ((S . i) . b)))
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
not a in dom (S . ((S .Lifespan() ) -' ((S . i) . b)))
let a, b be set ; :: thesis: ( a in dom (S . i) & b in dom (S . i) & (S . i) . a < (S . i) . b implies not a in dom (S . ((S .Lifespan() ) -' ((S . i) . b))) )
assume that
A1: a in dom (S . i) and
b in dom (S . i) and
A2: (S . i) . a < (S . i) . b ; :: thesis: not a in dom (S . ((S .Lifespan() ) -' ((S . i) . b)))
set CSI = S . i;
set VLI = S . i;
set GN = S .Lifespan() ;
set k = (S .Lifespan() ) -' ((S . i) . a);
set j = (S .Lifespan() ) -' ((S . i) . b);
set CSJ = S . ((S .Lifespan() ) -' ((S . i) . b));
set VLJ = S . ((S .Lifespan() ) -' ((S . i) . b));
set CSK = S . ((S .Lifespan() ) -' ((S . i) . a));
set VLK = S . ((S .Lifespan() ) -' ((S . i) . a));
(S . i) . b <= S .Lifespan() by Th22;
then A3: (S .Lifespan() ) -' ((S . i) . b) = (S .Lifespan() ) - ((S . i) . b) by XREAL_1:235;
(S . i) . a <= S .Lifespan() by Th22;
then A4: (S .Lifespan() ) -' ((S . i) . a) = (S .Lifespan() ) - ((S . i) . a) by XREAL_1:235;
1 <= (S . i) . a by A1, Th22;
then A5: (S .Lifespan() ) -' ((S . i) . a) < S .Lifespan() by A4, XREAL_1:46;
assume A6: a in dom (S . ((S .Lifespan() ) -' ((S . i) . b))) ; :: thesis: contradiction
A7: S .PickedAt ((S .Lifespan() ) -' ((S . i) . a)) = a by A1, Th27;
(S .Lifespan() ) -' ((S . i) . b) < (S .Lifespan() ) -' ((S . i) . a) by A2, A3, A4, XREAL_1:17;
then S . ((S .Lifespan() ) -' ((S . i) . b)) c= S . ((S .Lifespan() ) -' ((S . i) . a)) by Th24;
then dom (S . ((S .Lifespan() ) -' ((S . i) . b))) c= dom (S . ((S .Lifespan() ) -' ((S . i) . a))) by RELAT_1:25;
hence contradiction by A5, A6, A7, Def27; :: thesis: verum